The tag has no wiki summary.

learn more… | top users | synonyms

1
vote
1answer
55 views

CTL and LTL logic difference

I am trying to understand these subtle differences between LTL and CTL logic and one thing I simply don't have an idea how to understand. Formula AG AF p in ...
0
votes
0answers
51 views

What is the difference between LTL connectives X and O?

I have seen two different sets of connectives for LTL (see the picture): I have learned LTL by the connectives of the first column ($X, F, G,$ ...). The table (from Wikipedia) says that the ...
1
vote
2answers
67 views

Resource for LTL formulae?

I would like to practice on some problems for using LTL formulae but besides the foundations and theory there are only every few examples. I know that having understood theory is not enough. Where can ...
-1
votes
1answer
75 views

Constructing automata with the same traces, but where a CTL-formula is not equally satisfied [closed]

Hard to put this question in a short title. As part of a self-exercise, I'm trying to solve 6.15b of Principles of Model Checking by Baier and Katoen. You're supposed to prove that there does not ...
3
votes
2answers
183 views

Relation between interval temporal logic and linear temporal logic

I am trying to understand the relation between interval temporal logic and linear temporal logic. Do the two form of expressing temporal constraints have the same expressive power, or is one of the ...
1
vote
1answer
184 views

How to show that ECTL* is more expressive than CTL* $\cup$ Büchi (with an example)

I am looking for a preferably simple property that is expressible in ECTL* but not in CTL* and not in B├╝chi, with a citable reference to the proof. Details of what I've tried: I've tried a ...
5
votes
1answer
152 views

What is the complexity of model checking Process Logic (LTL fragment)?

Process Logic is a modal logic allowing to reason about temporal properties of programs. Its formulae take the form similar to (Propositional) Dynamic Logic $[P]\phi$, with $P$ being a program (think ...
0
votes
0answers
89 views

Temporal Logic and Access Control Models

What is the best way to describe the semantics of a new access control model?. I heard the temporal logic is the way to go. Is it true?
0
votes
1answer
139 views

Implicit Non-deterministic Buchi determinization

I am doing implicit Buchi determination for LTL logic in hardware where the combinational logic represents the set of states. But instead of using acceptance states, I am using final state (as in ...
-1
votes
1answer
193 views

problem in embedding

I want to embed PPTL(a kind of logic) in Coq. Because of its complex semantics, I just embed its systax. ...
4
votes
1answer
203 views

What is an unambiguous language in the sense of Schützenberger?

I'm reading Thomas Wilke's survey on the connections between Temporal Logic and finite automata, finite semigroups and first-order logic. In Theorem 6 (by Kamp), the fragment ...
7
votes
2answers
276 views

What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?

I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation. For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want ...
16
votes
2answers
897 views

Trace Equivalence vs LTL Equivalence

I am looking for an easy example of two transition systems that are LTL equivalent, but not trace equivalent. I have read the proof of Trace Equivalence being finer than LTL Equivalence in the book ...