The 2024 Developer Survey results are live! See the results

# 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.

20 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
850 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 ...
184 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 ...
• 41
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, ...
• 5,756
54 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 ...
• 121
349 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 ...
109 views

• 203
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 ...
10 views

### Counterexample Construction and Translation in CEGAR

As in this slide, M2 is an abstraction of M1 using the abstraction function f1 which essentially groups based on labels. Then we see that the property is not satisfied by the abstraction so we find ...
• 80
18 views

### When does Simulation Equivalent imply Bisimulation

Here, Given 2 Kripke structures M1 and M2, if there exists a simulation from M1 to M2 and a simulation from M2 to M1, is there a bisimulation from M1 to M2?, it is shown that for two LTSs M1 and M2 ...
• 80
17 views

### LTL Model Checking Worst Case size for NBA

I have a slide that gives the worst case time complexity of LTL model checking which uses a product construction of an LTS along with the NBA for the negation of the LTL formula. My question is, when ...
• 80
16 views

### Irregular Safety Properties

A regular safety property is a safety property whose bad prefixes form a regular language, https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec4.pdf. My questions is, are there ...
• 80
39 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 ...
577 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 ...
250 views

### Show the formula is a law of LTL

Show that the following formula is a law of LTL, i. e. the formula is satisfied on all paths in all models G(p → X q) ∧ G(q → F p) ∧ p → G F p I dont know how ...
• 173