The linear-temporal-logic tag has no wiki summary.
-1
votes
1answer
45 views
Constructing automata with the same traces, but where a CTL-formula is not equally satisfied
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 ...
2
votes
1answer
113 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 ...
0
votes
1answer
114 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
107 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
84 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
128 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 ...
0
votes
0answers
65 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
187 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 ...
6
votes
2answers
236 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 ...
15
votes
2answers
826 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 ...
