Skip to main content

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

Filter by
Sorted by
Tagged with
6 votes
0 answers
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 ...
generic_logician's user avatar
0 votes
0 answers
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 ...
timtombobjohn's user avatar
1 vote
1 answer
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 ...
user1868607's user avatar
  • 1,049
2 votes
0 answers
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 ...
Karl 17302's user avatar
2 votes
0 answers
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 ...
Nicola Gigante's user avatar
1 vote
0 answers
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 ...
Yann TM's user avatar
  • 111
1 vote
1 answer
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 ...
wanderingmathematician's user avatar
2 votes
1 answer
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$ ...
wanderingmathematician's user avatar
1 vote
1 answer
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 ...
ahelwer's user avatar
  • 151
1 vote
1 answer
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 ...
Tyler Durden's user avatar
1 vote
1 answer
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 ...
kauray's user avatar
  • 135
-1 votes
2 answers
175 views

Linear temporal logic in computational trees

I came across these slides while learning about the differences between CTL and LTL and am confused about what is written in the last slide. The problem is proving that $GF p \implies GF q$ and $ AG ...
Akshit's user avatar
  • 103
1 vote
1 answer
89 views

Proving liveness-like property on an infinite tree

(Context: this is a problem from the middle of my dissertation work, abstracted into a more general problem. It's related to showing that some liveness properties hold, so perhaps work from something ...
Jonathan Schuster's user avatar
3 votes
0 answers
130 views

Family of formulas for which Gabbay's separation algorithm explodes nonelementarily

It is repeated throughout the literature that Gabbay's algorithm for separation of LTL with Since and Until can produce nonelementary blow-up of the size of the formula, but I have never seen a proof ...
Daniel Oliveira's user avatar
4 votes
1 answer
241 views

resolution based theorem prover for temporal logic

I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are ...
Motorhead's user avatar
  • 181
1 vote
2 answers
73 views

Algorithms to synthesize optimal plans satisfying temporal logic constraints

I know how NuSMV can be applied on a model to check if certain temporal logic statements are satisfied, particularly LTL. I also know of the LTL to BA conversion routines available online. I am ...
user_1_1_1's user avatar
2 votes
0 answers
121 views

Applications of the monoidal closed structure in LTL?

A simple model of temporal logic is via time-indexed truth functions. This lets us model the Boolean connectives, as well as the next-step operator and modal always operator: $$ \begin{array}{lclll} ...
Neel Krishnaswami's user avatar
1 vote
0 answers
540 views

Safety properties in CTL

In the literature, I have only found a formal definition for safety properties in LTL. This, essentially, boils down to the following: "every trace that violates the property has a finite prefix ...
Simon Bliudze's user avatar
5 votes
1 answer
216 views

Complexity of propositional LTL with past operators and freeze quantifier?

In "A Really Temporal Logic", by R.Alur and A.Henziger, they introduce an extension of Linear Temporal Logic with a freeze quantifier $x.\phi$, which allows to "give a name" to the current time point ...
Nicola Gigante's user avatar
-1 votes
1 answer
149 views

Global satisfiability in LTL

In propositional linear temporal logic (LTL) over $\mathbb{N}$, it is decidable whether a formula $\varphi$ is satisfiable from time point 0. Is it known to be un/decidable to check the ...
Tyler Durden's user avatar
0 votes
0 answers
153 views

Approximating liveness properties with safety properties

Given a finite alphabet set $\Sigma$, the set $\Sigma^{\omega}$ of infinite words over $\Sigma$ can be topologized with a metric $d: \Sigma^{\omega} \rightarrow \mathbb{R}$ such as: $\forall w_1, w_2 ...
Ahmed Nassar's user avatar
1 vote
1 answer
749 views

Regular safety properties and bad prefixes of $\omega$-regular properties

I have two questions: By starting with a nondeterministic Büchi automaton (NBA) $\mathcal{A}^{\varphi} = (Q, \Sigma, \rightarrow, I, F )$ for an $\omega$-regular property $\varphi$, we can construct ...
Ahmed Nassar's user avatar
5 votes
2 answers
263 views

Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso?

Are there linear time temporal logics that can express some property $P_{nonlasso}$ that does have a counterexample, but none that is a lasso (or finite)? Details: One advantage of model checking ...
DaveBall aka user750378's user avatar
2 votes
1 answer
234 views

Reference for CTL* logic

I need a reference for CTL* logic (preferably easy to understand). I have gathered some disperse information regarding temporal and CTL logic but I need a more orderly coverage. A chapter of the ...
wmac's user avatar
  • 129
5 votes
1 answer
646 views

Calculating least fixed points in equations

Given a set of relations/equations in some logic like LTL would it be possible to find a least fixed point for those equations? For example take the equations in LTL $$ P = Play ~\land X(P \cup S)\\ ...
epsilon_0's user avatar
8 votes
2 answers
3k views

Do past time LTL and future time LTL have the same expressiveness?

I would like to ask if anybody is aware of a paper comparing the expressiveness of past time LTL and that of (future time) LTL.
sean's user avatar
  • 722
-4 votes
1 answer
178 views

Temporal Logic - Until [closed]

I have a doubt, in Linear Temporal Logic LTL, does the Until operator require that the first occurrence is the first term of the formula? ex: a U b does require ...
Nk SP's user avatar
  • 131
1 vote
2 answers
4k views

LTL property - safety or liveness?

How can I check if an LTL (Linear Temporal Logic) property is safety or liveness? Is it right to say that a property is safety OR liveness (or neither)? How can I evaluate this: ...
Nk SP's user avatar
  • 131
5 votes
0 answers
194 views

Are there any logics to formalize understanding?

Are there any logics (modal-based or others) to formalize the following statement: "agent A understands p". For example "agent A understands that Titanic sank because it hit an iceberg" Where "...
user avatar
0 votes
0 answers
94 views

A self-contained proof that OrdHorn relations are tractable?

I'm currently investigating a family of temporal relations called 'Ordered Horn' ($OH$ for short). This class was introduced in 'Reasoning about Temporal Relations: A Maximal Tractable Subclass of ...
NisaiVloot's user avatar
  • 1,292
3 votes
1 answer
4k views

CTL and LTL logic difference

I am trying to understand these subtle differences between LTL and CTL logic and one thing I simply don't have an idea how to understand. Formula AG AF p in ...
darxsys's user avatar
  • 133
2 votes
0 answers
505 views

Conversion technique/tool from temporal logic CTL,CTL* or LTL to μ-calculus

Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
Dimiter's user avatar
  • 39
2 votes
0 answers
167 views

Satisfiability of circuits with infinite input

As we all know, satisfiability of Boolean circuits is NP-complete. I am wondering if there are any studies of circuits with infinite inputs? That is, suppose the input is from the set $\{0,1\}^\omega$...
Shaull's user avatar
  • 5,656
4 votes
2 answers
317 views

Relation between interval temporal logic and linear temporal logic

I am trying to understand the relation between interval temporal logic and linear temporal logic. Do the two form of expressing temporal constraints have the same expressive power, or is one of the ...
Mirko's user avatar
  • 41
1 vote
1 answer
583 views

How to show that ECTL* is more expressive than CTL* $\cup$ Büchi (with an example)

I am looking for a preferably simple property that is expressible in ECTL* but not in CTL* and not in Büchi, with a citable reference to the proof. Details of what I've tried: I've tried a ...
DaveBall aka user750378's user avatar
9 votes
1 answer
1k views

CTL* and mu-calculus

it is well known that the modal $\mu$-calculus is one of the most expressive temporal logics for expressing properties of trees/graphs, and that CTL* is strictly less expressive than the $\mu$-...
LORE81's user avatar
  • 111
5 votes
1 answer
570 views

What is the complexity of model checking Process Logic (LTL fragment)?

Process Logic is a modal logic allowing to reason about temporal properties of programs. Its formulae take the form similar to (Propositional) Dynamic Logic $[P]\phi$, with $P$ being a program (think ...
walkmanyi's user avatar
  • 153
3 votes
2 answers
256 views

Alternating automata

In the paper Fast LTL to Buchi Automata Translation (2001, Gastin and Oddoux) the authors, while defining co-Buchi alternating automata define $\Sigma’= 2^\Sigma$ where $\Sigma$ is the alphabet. ...
pratibha sawhney's user avatar
4 votes
2 answers
393 views

Inductive definition of ECTL*: how are recursive formulas forbidden?

In [1], the extended computation tree logic ECTL* is inductively defined as the propositional formulas over all E($A(F_1,..F_n)$), where E is the existential path quantifier and $A$ some Büchi ...
DaveBall aka user750378's user avatar
-1 votes
2 answers
2k views

Kripke model and LTL vs CTL formulae interpretation [closed]

I have this Kripke model $M$: $$ \begin{array}{ccccccc} \to & (p, q) & \to & (\neg p, \neg q) & \to & (p, \neg q) \\ & \circlearrowright & & & & \...
dendini's user avatar
  • 119
12 votes
2 answers
1k views

Expressiveness of Büchi vs CTL(*)

What is the relationship between the expressiveness of LTL, Büchi/QPTL, CTL and CTL*? Can you give some references that cover as many of these temporal logics as possible (especially between linear- ...
DaveBall aka user750378's user avatar
14 votes
2 answers
20k views

What is the difference between LTL and CTL?

I already read examples of formulas in CTL but not in LTL and vice-versa, but I'm having trouble gaining a mental grasp on LTL formulas and really what, at the heart, is the difference.
Anonymous Coward's user avatar