Questions tagged [temporal-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0
votes
1answer
84 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 ...
-1
votes
2answers
72 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 ...
1
vote
1answer
74 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 ...
3
votes
0answers
125 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 ...
4
votes
1answer
150 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 ...
1
vote
2answers
56 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 ...
2
votes
0answers
110 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} ...
1
vote
0answers
208 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 ...
5
votes
1answer
110 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 ...
-1
votes
1answer
105 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 ...
0
votes
0answers
98 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 ...
1
vote
1answer
512 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 ...
5
votes
2answers
214 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 ...
2
votes
1answer
211 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 ...
4
votes
1answer
268 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)\\ ...
5
votes
2answers
1k 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.
-4
votes
1answer
85 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 ...
1
vote
2answers
2k 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: ...
5
votes
0answers
187 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 "...
0
votes
0answers
89 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 ...
2
votes
1answer
3k 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 ...
2
votes
0answers
284 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 ...
2
votes
0answers
141 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$...
4
votes
2answers
282 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 ...
1
vote
1answer
386 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 ...
9
votes
1answer
931 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$-...
5
votes
1answer
425 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 ...
2
votes
2answers
234 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. ...
4
votes
2answers
301 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 ...
-1
votes
2answers
1k 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 & & & & \...
12
votes
2answers
700 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- ...
11
votes
2answers
11k 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.