Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [linear-temporal-logic]

The tag has no usage guidance.

-1
votes
2answers
64 views

Linear temporal logic in computational trees

I came across these slides while learning about the differences between CTL and LTL and am confused about what is written in the last slide. The problem is proving that $GF p \implies GF q$ and $ AG ...
3
votes
0answers
122 views

Family of formulas for which Gabbay's separation algorithm explodes nonelementarily

It is repeated throughout the literature that Gabbay's algorithm for separation of LTL with Since and Until can produce nonelementary blow-up of the size of the formula, but I have never seen a proof ...
3
votes
0answers
44 views

Structural property of DFAs/NFAs accepting LTL-definable languages

I consider LTL on finite words. In this context, there are a couple of nice equivalence results for a language L: L is LTL-...
5
votes
1answer
142 views

resolution based theorem prover for temporal logic

I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are ...
1
vote
2answers
180 views

Syntactic characterisation of the intersection of CTL and LTL

The Baier and Katoen textbook references this paper E. M. Clarke and I. A. Draghicescu. Expressibility results for linear-time and branching-time logics, pages 428–437. Springer Berlin ...
1
vote
0answers
160 views

Safety properties in CTL

In the literature, I have only found a formal definition for safety properties in LTL. This, essentially, boils down to the following: "every trace that violates the property has a finite prefix ...
4
votes
1answer
81 views

Complexity of propositional LTL with past operators and freeze quantifier?

In "A Really Temporal Logic", by R.Alur and A.Henziger, they introduce an extension of Linear Temporal Logic with a freeze quantifier $x.\phi$, which allows to "give a name" to the current time point ...
-1
votes
1answer
98 views

Global satisfiability in LTL

In propositional linear temporal logic (LTL) over $\mathbb{N}$, it is decidable whether a formula $\varphi$ is satisfiable from time point 0. Is it known to be un/decidable to check the ...
5
votes
2answers
211 views

Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso?

Are there linear time temporal logics that can express some property $P_{nonlasso}$ that does have a counterexample, but none that is a lasso (or finite)? Details: One advantage of model checking ...
4
votes
1answer
215 views

Calculating least fixed points in equations

Given a set of relations/equations in some logic like LTL would it be possible to find a least fixed point for those equations? For example take the equations in LTL $$ P = Play ~\land X(P \cup S)\\ ...
5
votes
2answers
1k views

Do past time LTL and future time LTL have the same expressiveness?

I would like to ask if anybody is aware of a paper comparing the expressiveness of past time LTL and that of (future time) LTL.
1
vote
2answers
2k views

LTL property - safety or liveness?

How can I check if an LTL (Linear Temporal Logic) property is safety or liveness? Is it right to say that a property is safety OR liveness (or neither)? How can I evaluate this: ...
2
votes
1answer
2k 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
223 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
249 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
98 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 ...
4
votes
2answers
279 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
364 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
401 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 ...
1
vote
1answer
183 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
155 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 ...
-2
votes
1answer
247 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. ...
6
votes
1answer
307 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 $\mathrm{TL}[\mathsf{F},\...
7
votes
2answers
460 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 ...
17
votes
2answers
1k 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 "...