CODEWITHSUNDEEP
model-checking
Jens Müller
Jens Müller

Reputation: 402

Temporal logic for modelling events at discrete points in time causing states/changes over a period of time

I am looking for an appropriate formalism (i.e. a temporal logic) to model the following kind of situation

  1. There can be events happening at discrete events in time (subject to conditions to be detailed below).
  2. There is state. This state cannot be expressed by a fixed number of variables. However, it is possible to express it with a linear list/array, where each entry consists of a finite number of variables.
  3. Before any events have happened, the state is fixed.
  4. At any point in time, events are possible. They have a fixed structure (with a few variables). The possible events are constrained by the current state.
  5. Events will cause an immediate change of the state.
  6. Events can also cause continuous state changes. For example, a variable (of one of the entries of the array mentioned above) changes its value from 0 to 1 over some time (either immediately or after a specified delay).
  7. It should also be possible to specify discrete points in time in the form "the earliest point in time after event E where some condition C holds", and to start a continuos state change at such a point.

Is there an existing temporal logic to model something like this?

It should also be possible to express desired conditions, like the following:

  1. Referring to a certain point in time: The sum of a specific variables of all the entries of the array may not exceed a certain threshold.
  2. Referring to change over time: For all possible time intervals, the value of a certain variable (again, from each entry of said array) [realistically, rather of some arithmetic expression computed for each entry] must not change faster than a given threshold.

There should exist a model checker that can check whether for all possible scenarios, all the conditions are met. If this is not the case, it should print one possible scenario and tell me which condition is not met. In other words, it should distinguish between conditions describing the possible scenarios, and conditions that have have to be fulfilled in those scenarios, and not just tell me "not possible".

Upvotes: 0

Views: 75

Answers (1)

Serge
Serge

Reputation: 3765

You need a model checker with more flexible language. Technically speaking model checking of systems of infinite state space is open research problem and in general case algorithmically undecidable. The temporal logic is more typically related to propreties under the question.

Considering limited info you shared about your project, why do not you try Spin/Promela it is loosely inspired by C and has 'buffers' which can be considered to be arrays. At the least you might be able to simulate your system?

Upvotes: 0

Related Questions