The tag has no wiki summary.

learn more… | top users | synonyms

1
vote
1answer
82 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
111 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)\\ ...
2
votes
2answers
169 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
55 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 ...
0
votes
2answers
102 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: ...
3
votes
0answers
158 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
71 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 ...
1
vote
1answer
129 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
127 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
110 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 ...
3
votes
2answers
203 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
220 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
401 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 ...
5
votes
1answer
186 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
212 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
254 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 ...
-2
votes
2answers
633 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 & & & & ...
10
votes
2answers
460 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- ...
7
votes
2answers
4k 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.