## 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

- Log in to post comments