18
votes
Accepted
Do past time LTL and future time LTL have the same expressiveness?
The quick summary is that LTL with only past and no future modalities defines properties expressed over finite-words and these are the star-free subset of the regular languages. Standard LTL when ...
- 12.3k
9
votes
Accepted
CTL and LTL logic difference
There are already some rather good related answers regarding LTL versus CTL. In a nutshell, LTL is first and foremost a logic of traces, and an LTL formula is true for a transition system $S$ if and ...
- 2,470
8
votes
Do past time LTL and future time LTL have the same expressiveness?
The logics are expressively the same, though past operators make LTL exponentially more succinct.
You can start here, from which there are references.
- 5,261
5
votes
LTL property - safety or liveness?
Your first question is answered in this paper: https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf
Given an LTL formula, translate it into a Büchi automaton, and remove states that have ...
- 1,175
4
votes
Accepted
Calculating least fixed points in equations
In general, we look at fixed-points of monotone functions over lattices, i.e. with some partial ordering over your elements.
If your lattice is complete (it has a least and greatest element, called a ...
- 2,724
3
votes
Accepted
Are both safety and liveness properties closed under finite intersection?
Safety properties are closed under finite intersection. This can be seen by following Alpern and Schneider's characterisation which showed that safety properties are limit-closed when viewed ...
- 800
3
votes
Accepted
Is every countable, finite-branching LTS bisimilar to a tree?
Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree.
Q2: No, by a cardinality argument. For instance take infinite binary trees with $L=\{a,b\}$. Each tree has countable set of states ...
- 7,643
3
votes
Is modal $\mu$-calculus "equivalent" to bisimulation?
For Q1, the answer is yes if we consider image-finite systems: for all node $t$ and label $a$, the number of $a$-successors of $t$ must be finite. In this case you don't even need fixpoints of the $\...
- 7,643
3
votes
Accepted
Difference between CTMC, DTMC, and MDP
The "probabilistic" element in probabilistic model checking is that the system being checked is probabilistic, not that we add probabilities to an existing deterministic or non-deterministic system.
...
- 5,261
3
votes
Accepted
Complexity of propositional LTL with past operators and freeze quantifier?
The answer was buried in a small section of the same paper that I was citing. Adding past operators to TPTL, in contrast of what happens with LTL, causes a huge increase in complexity as the ...
- 1,112
2
votes
Accepted
Global satisfiability in LTL
The statement $\langle M,i\rangle\models \varphi$ for all $i\in \mathbb{N}$ is equivalent to $\langle M,0\rangle\models G\varphi$. Thus, you can check the latter.
- 5,261
2
votes
Accepted
Regular safety properties and bad prefixes of $\omega$-regular properties
Your construction for bad prefixes is not correct on NBA's.
For instance take the NBA on alphabet $A=\{a,b\}$ with two initial states $q_a$ and $q_b$ where for both $x\in A$, $q_x$ goes to an ...
- 7,643
2
votes
Accepted
Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso?
Pierre Wolper defined in 1983 extended temporal logic (ETL, in Information and Computation 56, 72–99, doi:10.1016/S0019-9958(83)80051-5), where a temporal operator $\mathcal A(\varphi_1,\dots,\...
- 3,314
2
votes
Equivalent formula for LTL with and without past operators
The "equally expressive" statement means that if a formula of PLTL is a statement about the future, i.e. if it's evaluated at the first instant $0$ of the time domain $\mathbb N$, then there exists an ...
- 7,643
2
votes
resolution based theorem prover for temporal logic
Your translation goes into Presburger arithmetic, which is decidable.
You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. ...
- 31.6k
1
vote
Accepted
Linear temporal logic in computational trees
This question should (and will) probably be migrated to cs.se.
In the meantime, consider the computation tree of the depicted structure: in almost all paths, $p$ is seen only finitely often, making ...
- 5,261
1
vote
Algorithms to synthesize optimal plans satisfying temporal logic constraints
Maybe take a look at http://www.syntcomp.org/
This is a competition of tools solving the LTL synthesis problem (and some related problems).
- 366
1
vote
Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso?
I think it depends on what you mean by linear-time temporal logics. If you mean temporal logics that have linear time semantics (i.e. cannot distinguish more than trace equivalence, a la van Glabbeek) ...
- 366
1
vote
Reference for CTL* logic
See Venema, Yde. Temporal Logic. The blackwell guide to Philosophical Logic.
- 29
1
vote
Accepted
LTL property - safety or liveness?
To answer your second question: there is one property that is both safety and liveness: True. With this exception, however, it is fair to say that a property is either safety or liveness or neither. "...
- 366
Only top scored, non community-wiki answers of a minimum length are eligible