4 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 ...
Kai's user avatar
  • 854
4 votes
Accepted

Complexity of "discrete-time" SAT

Your problem is PSPACE-complete: Membership in PSPACE via a nondeterministic PSPACE algorithm: ...
Denis's user avatar
  • 8,678
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 ...
Nicola Gigante's user avatar
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 ...
Denis's user avatar
  • 8,678
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 $\...
Denis's user avatar
  • 8,678
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. ...
Shaull's user avatar
  • 5,571
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 ...
Denis's user avatar
  • 8,678
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.
Shaull's user avatar
  • 5,571
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. ...
Neel Krishnaswami's user avatar
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 ...
Shaull's user avatar
  • 5,571
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).
Markus's user avatar
  • 366

Only top scored, non community-wiki answers of a minimum length are eligible