我正在寻找一种适当的形式主义（即时间逻辑）来模拟以下情况
- 可能会有事件发生在离散的事件中（取决于下面详述的条件）。
- 有状态。这种状态不能用固定数量的变量来表达。但是，可以用线性列表/数组来表示它，其中每个条目由有限数量的变量组成。
- 在任何事件发生之前，状态是固定的。
- 在任何时间点，事件都是可能的。它们具有固定的结构（带有一些变量）。可能的事件受当前状态的约束。
- 事件将导致状态立即改变。
- 事件也可能导致持续的状态变化。例如，一个变量（上述数组的条目之一）在一段时间内（立即或在指定延迟后）将其值从 0 更改为 1。
- 还应该可以以“事件E之后某个条件C成立的最早时间点”的形式指定离散的时间点，并在该点开始连续的状态改变。
是否有现有的时间逻辑来模拟这样的事情？
还应该可以表达所需的条件，如下所示：
- 参考某个时间点：数组所有条目的某个特定变量的总和不能超过某个阈值。
- 提到随时间的变化：对于所有可能的时间间隔，某个变量的值（同样，来自所述数组的每个条目）[实际上，而不是为每个条目计算的某个算术表达式]的变化不得快于给定阈值。
应该有一个模型检查器，可以检查所有可能的场景是否满足所有条件。如果不是这种情况，它应该打印一个可能的场景并告诉我哪个条件不满足。换句话说，它应该区分描述可能场景的条件和在这些场景中必须满足的条件，而不仅仅是告诉我“不可能”。