During a run of an automaton are the important informations the of the automaton with the associated properties as well as the input events bound to the transitions. Input events are often also called actions caused by the environment. In the following semantical interpretations of the language the defintions make only use of the properties of the states (atomic propositions). Besides this it is possible -and in some situations necessary- to define also some meaning including possible input or output words.
The properties are given here as a set of atomic propositions.
If we have an automaton with a run we can identify a certain state of the automaton by referring to a position i in the execution of understood here as time i. It holds (e.g. if r is an ordered pair like then is the first projection of r ).
If a certain property is in -which is the same as - it states that the proposition is satiesfied by automaton in run at time i. Taking the proposition as an example of an expression of the language then one can write
Likewise one can represent the falseness of some in a certain state of a run of an automaton as
It is possible to define the truth of more complex expressions if one makes these expressions to arguments of logical operators like (negation, not) , (conjunction, and) , and (disjunction, or) . It shall hold that with then , , and are also in and it holds
Gerd Doeben-Henisch 2010-03-03