You are here

Temporal logics

Below one can find information on temporal logics handled by Verics, along with mmc-conv module description.

mmc-conv is an internal translator used by Verics GUI and usually is invisible for end users. It converts several timed automata formats together with temporal formulae files. Moreover it helps to determine which verification method is available to the given system and formula.

mmc-conv usage:
To display the help: mmc-conv -h
To convert to the Andrzej's format: mmc-conv -AZ filename
The fileneme is the name of the input file in the Intermediate Language (IL) format.
The output file name is the same as the input one but the ".in" extension is added for model  and "_form.in" is added for formula. It is also created a file with "_form.desc" extension where formula description is placed.

To get the product version: mmc-conv -version

To get the component type: mmc-conv -type 

 

  Output file format (AZ) is composed as follow: 

 

network
automaton
automaton
...
end

The automaton is defined as:

automaton

 

clocks number_of_cloks 

 

location location_number
[invariant]
end
 ...
  transition from_state to_state number_of_transition
[clock_constrain]
reset [nr_of_clock_to_reset]
end
...
valuation
[location_number propositional_variable_number [propositional_variable_number] ]
...
end

end 

 

 

All elements placed in square brackets are not obligatory. 

 

The number_of_clocks is the integer number corresponds to number of clocks in automaton. If no clocks are used the number of clocks is equal to zero.

 

In the locations declaration section the location_number are a integer numbers bigger or equal to 0 and must be unique in automaton.

 

The number_of_transition corresponds to transition name. It should be unique in the automaton and unique in all network. If the number_of_transition is the same on more than one transition in the network it means that this transition are synchronous. 

 

The nr_of_clock_to_reset is an integer number corresponding to clock that will be reset while transition is fired. If we don't want to reset any clocks the nr_of_clock_to_reset should be empty.

 

The propositional_variable_number is a integer number that corresponds to propositional variable used in input file. The mapping of propositional_variable_number to its names is given in formula output file. 

 

The invariant and the clock_constrain are expresions build with clocks for example x1 > 1, where x1 is first clock, > is relation function and 1 is clock value. 

 

The mmc-conv is now supporting LTL, CTL, CTLpK, CTLpKD, TCTL and CTL* formulae. They can build using rules: 

 

ctl - CTL formulae

 

A [ ctl1 U ctl2 ] - Always ctl1 Until ctl2
E [ ctl1 U ctl2 ] - Eventualy ctl1 Until ctl2
K [nr] (ctl) - agent nr Knows ctl
NK [nr] (ctl) - complementary for K
kk [nr][nr1,...,nrn](ctl) - agent nr Knows that agents nr1,...,nrn Knows ctl
dK [nr1,...,nrn](ctl) - Distributed Knowledge of agents nr1,...,nrn
NdK [nr,...,nr](ctl) - complementary for Distributed Knowledge
P [nr](ctl) - deontic operator
AG ctl - Always Global ctl
AF ctl - Always Finally ctl
AX ctl - Always in the next step ctl
EG ctl - Eventually Global ctl
EF ctl - Eventually Finally ctl
EX ctl - Eventually in the next step ctl
EF_ '<'|'(' time1 ':' time2 ')'|'>' ctl - timed version of EF
EU_ '<'|'(' time1 ':' time2 ')'|'>' ctl - timed version of EF
EG_ '<'|'(' time1 ':' time2 ')'|'>' ctl - timed version of EG
ER_ '<'|'(' time1 ':' time2 ')'|'>' ctl - timed version of ER
!ctl - negation operator
clt & ctl - conjunction operator
ctl + ctl - disjunction operator \

 

LTL formulae

 

F ltl - Finally ltl
G ltl - Globally ltl
X ltl - In the next step ltl
K [nr] (ltl) - agent nr Knows ctl
NK [nr] (ltl) - complementary for K
!ltl - newgation operand
ltl & ltl - conjunction operand
ltl + ltl - alternative operand
ltl U ltl - Untill operand

 

  CTL* formulae

 

!ctl* - negation operand
A ltl - Always ltl
E ltl - Eventually ltl
ctl* & ctl* - conjunction operand
ctl* + ctl* - alternative operand
ctl* U ctl* - Untill operand 

 

 

The formula output file contains original formula written in Reverse Polish Notation and mapping propositional variable names into their integer equivalents.

If in formula are used some timed expressions also time ranges are mapped into special type of variables and this mapping is writed down into this file.

 

For example formula ER_<0;7>(true, EF_<0;7>(S_Sender_ack) & R_Rec_bit0 & NK[2](S_Sender_ack) & (!R_Rec_bit0))  produce formula file containing: 

 

tp3EF[q2]p2&p3NK[2]&p-2&ER[q1]
q2 <0 >7
q1 <0 >7
end
# Map of translation of propositional variables names
# R_Rec_bit0 -> p2
# S_Sender_ack -> p3

 

and formula description file: 

ctl
temporal
non-epistemic
non-deontic
non-diagonal
timed
existential
operators:& 3;EF_ 1;ER_ 1;NK 1;t 1;~ 1 


Back to top