# Questions tagged [temporal-logic]

In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time

42 questions
Filter by
Sorted by
Tagged with
121 views

### How to prove clock equivalence is a time-abstracted bisimulation

An important step of developing the theory of timed automata is to reduce the question of reachability in the timed automata, which has infinitely-many states, to the question of reachability in an ...
77 views

### Number of quantifier alternations in prenex form of a formula

I'm currently studying hyperlogics and in particular HyperLTL/CTL*. In model checking algorithms for such logics the number of quantifier alternations appearing in a formula can play an important role ...
1 vote
176 views

### Complexity of "discrete-time" SAT

I'm interested in the complexity of deciding satisfiability of the following family of formulae: $\exists j. I[j(0)] \land \forall t. S[j(t),j(t+1)]$ where: $j:\mathbb{N} \to \{0,1\}^n$ has finite ...
• 1,049
89 views

### From formal models to programs - Model Checking

I am reading on Automata, Model Checking and CTL/LTL. I am looking for examples/references/books that help me understand the following: Given a program (for example Python or Java), how can I change ...
56 views

### Full version of the paper "Characterization of Temporal Property Classes"

Look at this paper: E. Chang, Z. Manna, A. Pnueli. "Characterization of Temporal Property Classes" The proof of Theorem 8 at page 8 says: "We will outline the proof which appears in the ...
• 1,628
1 vote
32 views

### Algorithm to decide if a CTL formula can also be expressed in LTL and translate it? [duplicate]

So I'm trying to solve some CTL formulas on a given system using model-checking. I'm trying several different solvers; some of them only accept LTL as input, but have some nice partial-order ...
• 111
1 vote
96 views

### Is every countable, finite-branching LTS bisimilar to a tree?

Let $L$ be a finite set of labels, and let $\mathcal{C}$ be the set of finitely-branching transition systems labeled by $L$ and with a countable set of states. Let $\sim$ denote the bisimulation ...
253 views

### Is modal $\mu$-calculus "equivalent" to bisimulation?

I know that propositional modal $\mu$-calculus $L\mu$ is bisimulation-invariant. However, I'm curious to what degree it captures bisimulation. Q1: Given two labeled transition systems $T_1$, $T_2$ ...
1 vote
2k views

### Difference between CTMC, DTMC, and MDP

I've been reading the Handbook of Model Checking recently; I'm especially interested in probabilistic model checking, so have been led to the PRISM model checker. For background, I am very familiar ...
• 151
1 vote
356 views

### Equivalent formula for LTL with and without past operators

I have recently been researching LTL with and without past operators. From my understanding, both LTL and PLTL (LTL with Past) are equally expressive, however, PLTL is exponentially more succinct. I ...
• 115
1 vote
877 views

### Are both safety and liveness properties closed under finite intersection?

Given two safety properties $P_1$ and $P_2$, is their intersection $P_1 \cap P_2$ also a safety property? Similarly, if $P_1$ and $P_2$ are liveness properties, is $P_1 \cap P_2$ also a liveness ...
• 135
175 views

• 119