Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

557 users

0 votes

In general can someone please explain the differences between the three Temporal Logics?

I did take this as a reference but when the conversion between the Logics is asked in the exam I often do get confused about how the end result should look like. An explanation with an example would be extremely helpful.

I also get confused about what a state formula is and what a path formula is. A brief note on it would be great! 


Thanks in advance!

in * TF "Emb. Sys. and Rob." by (660 points)

1 Answer

0 votes
 
Best answer

To keep the answer short:

In LTL there are usually no quantifiers "A" or "E" as LTL was designed to talk about paths and thus it only consists of path formulas. According to this definition you are only allowed to use one quantification (a universal) on the outermost level to make it possible to use LTL to reason about states. Thus:

If your formula contains no "A" or "E" => LTL

If your formula starts with an "A" and contains no "A" or "E" otherwise => LTL

In CTL every temporal operator needs to be quantified, so in front of every "G", "F", "X", "[x U y]", "[x U y]", "[x B y]", "[x B y]", "[x W y]" or "[x W y]" (as well as the arrow variants) with x, y being other state formulas there needs to be either an "A" or an "E" quantifier. For this reason CTL can be transformed to mu-calculus easily as each quantified temporal operator is a state formula and thus can be described by a mu-calculus formula describing the exact same states. Thus:

If every temporal operator has an "A" or "E" directly in front of it => CTL

Due to these two definitions, LTL and CTL are almost contrary languages with the one describing "only" paths and the other one describing only states. Thus a translation is needed from one to the other while preserving the meaning which is not always possible.

CTL* on the last side combines both, so there are no restrictions on whether a quantification must be there or must not be there, thus every syntactically "correct" formula is at least a CTL* formula (without going into detail, "correct" means that the formula as constructed has a logical meaning behind it, so [x UU y] is of course not "correct").

by (3.5k points)
selected by

Related questions

0 votes
1 answer
asked Aug 26, 2023 in * TF "Emb. Sys. and Rob." by calvet (250 points)
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...