Временная логика для моделирования событий в отдельные моменты времени, вызывающие состояния / изменения в течение определенного периода времени

Question

Я ищу подходящий формализм (то есть временную логику) для моделирования ситуации следующего типа

1. Могут быть события, происходящие в отдельные события во времени (при условии, что условия будут подробно описаны ниже).
2. Есть государство. Это состояние не может быть выражено фиксированным числом переменных. Тем не менее, это можно выразить с помощью линейного списка / массива, где каждая запись состоит из конечного числа переменных.
3. До того, как произошли какие-либо события, состояние фиксируется.
4. В любой момент времени события возможны. Они имеют фиксированную структуру (с несколькими переменными). Возможные события ограничены текущим состоянием.
5. События повлекут за собой немедленную смену государства.
6. События также могут вызывать постоянные изменения состояния. Например, переменная (одной из записей массива, упомянутых выше) меняет свое значение с 0 на 1 в течение некоторого времени (либо сразу, либо после указанной задержки).
7. Также должна быть возможность указать дискретные моменты времени в форме "самый ранний момент времени после события E, когда выполняется некоторое условие C", и начать непрерывное изменение состояния в такой точке.

Существует ли существующая временная логика для моделирования чего-то подобного?

Также должна быть возможность выразить желаемые условия, такие как следующее:

1. Обращение к определенному моменту времени: сумма определенных переменных всех записей массива не может превышать определенный порог.
2. Обращаясь к изменению во времени: для всех возможных временных интервалов значение определенной переменной (опять же, из каждой записи указанного массива) [реально, а не некоторого арифметического выражения, вычисленного для каждой записи], не должно изменяться быстрее, чем заданный порог.

Должна существовать программа проверки моделей, которая может проверить, соблюдаются ли для всех возможных сценариев все условия. Если это не так, он должен напечатать один возможный сценарий и сказать мне, какое условие не выполняется. Другими словами, он должен различать условия, описывающие возможные сценарии, и условия, которые должны быть выполнены в этих сценариях, а не просто говорить мне "невозможно".

Answer 1

Вам нужна программа проверки моделей с более гибким языком. С технической точки зрения проверка моделей систем с бесконечным пространством состояний является открытой исследовательской проблемой и в общем случае алгоритмически неразрешимой. Темпоральная логика чаще связана с рассматриваемыми свойствами.

Учитывая ограниченную информацию, которой вы поделились о своем проекте, почему бы вам не попробовать Spin/Promela, он основан на C и имеет "буферы", которые можно рассматривать как массивы. По крайней мере, вы могли бы смоделировать свою систему?