5 votes
Accepted

Translation of Counter-free automata into Linear Temporal Logic

As mentioned in the comments, the translation is shown in: Volker Diekert and Paul Gastin. "First-order definable languages." (2008) http://www.lsv.fr/Publis/PAPERS/PDF/DG-WT08.pdf And it ...
Shaull's user avatar
  • 5,571
4 votes

Translation of Counter-free automata into Linear Temporal Logic

Sorry to provide the same answer as for this question, but this was proved in [1, Theorem 3.1]. [1] J. Cohen, D. Perrin and J.-É. Pin, On the expressive power of temporal logic for finite words, J. ...
J.-E. Pin's user avatar
  • 4,781
4 votes

Reference request: An algebraic characterisation of LTL[XF]-definable word languages

An algebraic characterisation of the restricted temporal logic (fragment using only next and eventually, but not until) is given in [1]. The expressive power of this fragment is the set of regular ...
J.-E. Pin's user avatar
  • 4,781
3 votes
Accepted

Decomposition of safety and liveness properties

Yes. The automata in question are often called "Looping" automata (so you have a keyword to start from). A possible starting point is the following paper: https://faculty.idc.ac.il/udiboker/...
Shaull's user avatar
  • 5,571
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
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
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
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

Reference request: An algebraic characterisation of LTL[XF]-definable word languages

I've just found an answer to my question. It is inside Bojańczyk's notes titled "Languages recognised by finite semigroups and their generalisations to objects such as trees and graphs with an ...
Bartosz Bednarczyk's user avatar
2 votes
Accepted

Why does LTL equivalence (with next oeprator) implie trace equivalence in finite transition machines?

The important thing to notice is that in finite transition systems, two systems $K_1,K_2$ over an alphabet $\Sigma$ are not trace equivalent (for infinite traces) if and only if there exists a finite ...
Shaull's user avatar
  • 5,571
2 votes
Accepted

Proving that a given formula in LTL is the smallest way to express it

I'm not sure whether it would work in your case, but in order to show succinctness results in modal/temporal logic (e.g. the fact the two-variable logic over words in exponentially more succinct than ...
Bartosz Bednarczyk's user avatar
1 vote

Maximally Permissive Strategies for Safety Properties

In a safety game, the existence of a maximally permissive strategy is easy to show: you always allow all moves that stay in the winning region. This works because safety games are precisely the games ...
Denis's user avatar
  • 8,678
1 vote

Proving that a given formula in LTL is the smallest way to express it

Your question is formally the same as this one: how many symbols $X$ are needed to write the polynomial $XX + XXXX + XXXXXX = XX(1 + XX(1 + XX))$? Well, you obtained $6$ as an upper bound. It is also ...
J.-E. Pin's user avatar
  • 4,781
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

Syntactic characterisation of the intersection of CTL and LTL

Note that by "equivalent", we actually need to interpret LTL over trees. Thus, we say that a CTL formula $\phi$ is equivalent to an LTL formula $\psi$, if $\phi$ is equivalent to the CTL* formula $A\...
Shaull's user avatar
  • 5,571
1 vote

Temporal Logic and Access Control Models

There were a lot of publication on extending and or formalizing RBAC/SOD with LTL or other flavors of temporal logics, not sure of other AC models. Google Scholar (or simple google) search with yield ...
Serge's user avatar
  • 111

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