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
13
votes
1
answer
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 ...
- 411
4
votes
0
answers
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 ...
- 41
3
votes
0
answers
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,359
2
votes
0
answers
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 ...
- 121
2
votes
0
answers
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 ...
2
votes
0
answers
107
views
Satisfying of $\square (\neg A \cup B)$
Let's consider the following formula:
$\square (\neg A \cup B)$.
Does the following computation satisfy it?
The numbers in brackets are number of state.
(0) $\neg A, \neg B$
(1) $\neg A, B$
(2) $...
user68041
2
votes
0
answers
34
views
BDI logic or KARO framework solver - are there solvers for any new logic?
I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
- 1,381
1
vote
0
answers
20
views
About next operator duality in LTL
I'm learning LTL (linear temporal logic) and we learned that a model $M$ and a starting position $q_0$ satisfies a LTL formula $\psi$ iff for every path $\pi$ starting at $q_0$ it is true that $\pi \...
- 111
1
vote
0
answers
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,045
1
vote
1
answer
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$ ...
- 111
1
vote
1
answer
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....
user127009
1
vote
0
answers
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 ...
- 11
1
vote
0
answers
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^*...
- 203
1
vote
0
answers
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 ...
- 11
0
votes
0
answers
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?
- 227
0
votes
0
answers
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 ...
0
votes
0
answers
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 ...
- 1
0
votes
0
answers
241
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
-1
votes
0
answers
23
views
Validity of ♢(p ∨ q) → ¬□(¬p ∨ ¬q) in linear temporal logic
Let p, q denote propositional variables and ϕ, ψ denote LTL formulas. Is the following LTL formulas is valid?
♢(p ∨ q) → ¬□(¬p ∨ ¬q)
and how to proof using A not satisfying word is σ1,unsat := {p}∅∅......
- 1