2022 Developer Survey is open! Take survey.

# Tag Info

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
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

### 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,246

### 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
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 ...
• 5,246

### 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. ...
• 4,721

### 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 ...
• 4,721
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
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/...
• 5,246
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,246
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
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,246
Accepted

• 5,246
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
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
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 ...
• 111

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