# Questions tagged [linear-temporal-logic]

LTL (linear temporal logic or linear-time temporal logic) is a temporal logic that can encode assertions about the future of traces.

19 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
779 views

### The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
181 views

### Understanding a proof from a paper (model checking game)

I'm reading the paper: "Model Checking Games for Branching Time Logics" by Martin Lange and Colin Stirling - https://carrick.fmv.informatik.uni-kassel.de/~mlange/papers/jlc2000.pdf. The ...
96 views

### Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
53 views

### Does Rice's theorem apply to sequential logic circuits?

I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any ...
324 views

### Equivalence preserving operator from CTL* to LTL

The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
107 views

1 vote
19 views

### Errors in examples of Vardi's paper "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces"

The paper Linear Temporal Logic and Linear Dynamic Logic on Finite Traces has the following examples on page 4: Q1. (Update to Q1: solved. See the comment by DCTLib.) The first example says that the ...
1 vote
168 views

### Translating Natural Language to LTL Formulae

I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct. I'm given the sentences, and my assumption is that $l$ ...
1 vote
99 views

### What does “linear” in Linear Temporal Logic refer to?

Consider the term linear temporal logic (in the meaning of linear-time temporal logic). In linear temporal logic, what does linear refer to: to temporal or to logic? If I interpret http://en.... 1 vote
226 views

### Unable to have an equivalent of A(FG p) and AG(EF p)

It states in my lecture notes that there is no CTL formula that is equivalent to A(FG p) in LTL and likewise, there is no LTL formula that is equivalent to CTL formula AG(EF p). I am just starting to ...
1 vote
144 views

### generic technique to build LTL/CTL formula that satisfy specific inputs to a model

I have an automaton, for example the below automaton and would like to generate a single formula (LTL or CTL, or some other representation) that satisfy exactly the traces provided. e.g., \$t_1 = i^*...
1 vote
49 views

### Size of parity automata and Buchi automata from linear time mu-calculus?

Given a linear time mu-calculus formula, there are many works on transforming the formula to Buchi or Parity automaton. Using the best algorithm, what is the size of the resulting Buchi automaton and ...
15 views

### Is first order linear temporal logic a special case of first order modal logic?

Propositional linear temporal logic is a special case of propositional modal logic. Is first order linear temporal logic likewise a special case of first order modal logic?
24 views

### Can an LTL formula uniquely be represented by an expression tree?

Just like we can represent a mathematical expression uniquely with a binary expression tree, I was wondering if we could do the same for LTL formulae? Such that no two different looking LTL formula ...
522 views

### How to draw a Non Deterministic Buchi Automaton (NBA) from the given property?

I'm new to LTL and Buchi automaton, and I have a hard time in constructing NBA from the given formula or the property. Could somebody please help me? The following property is given, P= "Whenever ...