All Questions
Tagged with linear-temporal-logic automata
15 questions
2
votes
1
answer
219
views
Büchi automaton to Linear Temporal Logic
Given a Büchi automaton what is the procedure to build an equivalent LTL formula? And what is its size?
I'm looking for references but I haven't found them so far.
- 401
1
vote
1
answer
496
views
LTL to Büchi automaton, deterministic?
I know it is possible to convert LTL formulas to Büchi automatons. But is it possible to convert a LTL formula to a deterministic Büchi automaton? Are there formulas that can't be converted to a ...
2
votes
2
answers
263
views
How to graph search a LTL-generated Buchi automaton to generate valid execution paths
I have a set of tasks, and a LTL specification that describes which orders of the tasks are legal. I want to find a way to enumerate all permutations of the tasks that meet the specification.
For ...
- 163
0
votes
1
answer
92
views
LTL to automaton translation that can only read disjunctions of labels per transition
Is there any automaton (or automaton translation) as expressive as LTL that can only read disjunctions of atomic propositions per each transition? Standard LTL-to-automaton algorithms allow the ...
- 175
4
votes
1
answer
269
views
Minimal Deterministic Buchi Automata Product
Problem:
Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas.
Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1)...
0
votes
1
answer
247
views
LTL to GBA versus LTL to BA
Let's assume that I have an LTL formula and I want to convert it to a Buchi automaton. For which fragment of LTL, GBA is more succinct and for which fragment BA has the same size as GBA.
- 175
1
vote
1
answer
174
views
What kind of LTL formula can be represented by DBAs
I am looking for the portion of LTL formula that can be expressed by deterministic buchi automata. Is there any classification of this such?
- 175
0
votes
1
answer
129
views
Buchi Automaton G(Xa->b)
I have a question regarding buchi automatons. The automata for the LTL formula, G(Xa->b) is as the attached picture. Why dosen't a have to be true in order to make the automaton correct?
My ...
- 1
7
votes
1
answer
406
views
Non-deterministic Büchi vs Rabin: Automaton size for LTL->automaton
Is there any general result to show that which automaton is more succinct? I have a set of LTL properties and I would like to know (show) which automaton is more efficient in term of state number and ...
- 175
2
votes
1
answer
245
views
Are there any LTL to _non_ deterministic Rabin automaton translators?
I know of two translators LTL -> deterministic Rabin automaton:
Rabinizer3
ltl2dstar
They produce deterministic automata, which can be much larger than their possible non-deterministic variants. Is ...
- 1,095
1
vote
0
answers
153
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
2
votes
0
answers
52
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 ...
- 21
3
votes
1
answer
532
views
Time to construct a GNBA for LTL formula
I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula:
Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
- 401
33
votes
2
answers
1k
views
Equivalence of Büchi automata and linear $\mu$-calculus
It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...
- 2,197
10
votes
1
answer
905
views
Algorithm to translate a deterministic Büchi automaton to LTL (when possible)
Linear temporal logic and deterministic Büchi automata are incomparable: DBA cannot express $FGa$, and LTL cannot express "at least each odd letter is 'a'". But sometimes it is interesting to know ...
- 1,095