Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [temporal-logic]

The tag has no usage guidance.

2
votes
1answer
35 views

Reasoning about resources: “resource logics”?

Are there extensions of predicate logic which focus on resource models, possibly even in actor models? And if so, would it be possible to reason on a meta-level on how many resources should be ...
3
votes
0answers
17 views

conversion of basic $\text{CTL}^*$ formulas to $\text{CTL}$

Consider the $\text{CTL}^*$ formula $E[pU(qUr)]$. It is not hard to show that it is equivalent to the $\text{CTL}$ formula $E[pU(EqUr)]$. The informal reason is that a path where $p$ is true until $...
0
votes
0answers
9 views

Timed Kripke structures with inequality constraints

I am having problems creating a timed Kripke structure $\mathcal{TK} = \langle S, \mathcal{T}, \rightarrow, L \rangle$ for a system that I have. My system, a timed automaton system (time base $\...
2
votes
1answer
27 views

How do you correctly write this sentence as a CTL formula?

Sentence: From every reachable state it is possible to reach a state where $p$ is true. How do you write this sentence as a CTL formula? So far I only dealt with CTL syntax and trees but maybe it ...
0
votes
1answer
29 views

distinguishing between CTL* formulas $A[FG p]$ and $AFAG p$ using transition system

It is to show, using a transition system, that the two formulas $A[FG p]$ and $AFAG p$ are not equivalent. For me, it seems strange that they are not equivalent. As the first one says that any ...
2
votes
1answer
59 views

Linear Temporal Logic (LTL) Syntax Infinitely Often

I'm a little confused about some LTL syntax. When the Global and Future operator (GFx) or []<>x is used, what does it mean. In the lecture slides it is given as infinitely often. But I don't ...
0
votes
0answers
32 views

Writing LTL formula for sequencing with coordination

Suppose there are 2 workers w1 and w2 who can cool a hot iron. So if iron is hot (denoted by atomic proposition ...
2
votes
2answers
54 views

How to graph search a LTL-generated Buchi automaton to generate valid execution paths

I have a set of tasks, and a LTL specification that describes which orders of the tasks are legal. I want to find a way to enumerate all permutations of the tasks that meet the specification. For ...
0
votes
1answer
44 views

Linear Temporal Logic, Idempotent law

in many lecture notes, I have seen the LTL idempotent law for until and its equivalence is described as $\phi U(\phi U \psi) \equiv \phi U\psi$ and also $(\phi U \...
0
votes
1answer
66 views

LTL globally implies

I have got confused in undressing the informal definition of LTL below: $$G(\phi \Longrightarrow\psi)\Longrightarrow(G\phi \Longrightarrow G\psi)$$ in many literatures I have seen implies is said as ...
1
vote
0answers
23 views

CTL satisfied by Kripke Structure

given a Kripke Structure I want to check if a CTL formula is satisfied or not. the CTL is: $$ AG(c \vee AX\neg E((a\vee b)Uc)) $$ I have read that it is better to write to CTL in terms of $\wedge $ ...
0
votes
0answers
16 views

Temporal logic - mixing AF and AG in CTL formula

Let's look at example AF(φ1 -> AG(φ2)). Does it mean that: In all paths it eventually happens that if φ1 was satisfied, φ2 is satisfied all along the path (so ...
0
votes
1answer
114 views

Can the foundation of computer science be implemented to include new rules of inference so that computer can do causal reasoning?

The idea I'm thinking of is about a top-down approach for AI. I would like to know if there can be a model for computers so that they can perform causal reasoning. It seems that causal relation can be ...
0
votes
1answer
54 views

Given two formulae E[G F p] (which is CTL*) and EG EF p ( which is a CTL) with a Model prove that they are not equivalent

I am trying to prove they are not equivalent , a model which satisfies the fist one but not the second since I think EG EF p is stronger than E[GF p],any leads would be helpful. Thanks.
1
vote
0answers
37 views

Unable to have an equivalent of A(FG p) and AG(EF p)

It states in my lecture notes that there is no CTL formula that is equivalent to A(FG p) in LTL and likewise, there is no LTL formula that is equivalent to CTL formula AG(EF p). I am just starting to ...
2
votes
0answers
68 views

How to know whether a formula is common knowledge in Kripke structure?

Suppose that we have a formula A which is valid in all states of Kripke structure and some transition relations. Is it generally possible to derive if formula A is common knowledge between particular ...
3
votes
1answer
80 views

CTL* query evaluation order

I'm currently trying to evaluate a CTL* expression and am not sure how to stepwisely evaluate the queries. For example I have EFG p. This means something like 'there is a path where eventually there ...
5
votes
2answers
351 views

Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators

Need to prove equivalence for (or disprove equivalence for): $ \hspace{1cm}\square ϕ → \lozenge ψ ≡ ϕ\textsf{ U }(ψ ∨ ¬ϕ) \\ $ My current attempt using the LTL equivalnce rules to determine ...
13
votes
1answer
381 views

The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
2
votes
1answer
93 views

What's the definition of ACTL?

I have been looking for the definition of ACTL, but Google has given me very little to go with. So far, I know ACTL is another form of CTL model checking, and CTL includes the following operators: ...
2
votes
1answer
294 views

What are the differences between propositional logic and temporal logic?

I am currently studying temporal logic and find it much similar to propositional logic. However, temporal logic seems to be slightly more specific because it encapsulates more precise meaning symbols, ...
0
votes
1answer
242 views

Counterexample for LTL - CTL equivalence [closed]

I have to find an example of a model where the LTL-formula $F G p \wedge F q$ is valid and the CTL-formula $EF AG p \wedge AF q$ is not valid. I found this example, but I'm not completely sure whether ...
0
votes
1answer
238 views

Given a set of LTL formulas, on which states does the Kripke structure hold? [closed]

I'm currently learning about LTL and CTL formulas and to get a better understanding I try to manually interpret the formulas over a given Kripke structure. Since I'm not 100% sure if my results are ...
5
votes
2answers
150 views

Modeling concurrent algorithms

I'm working on a class library (C++) that can be thought of as a producer/consumer queue of producer/consumer queues. There are many queues of data, and the goal is to assign worker threads to process ...
1
vote
1answer
191 views

CTL - model checking for formula $A [a \cup b]$

I'm trying to verify if the following model satisfy $A [a \cup b]$: The algorithm I'm using is taken from "Concepts, Algorithms, and Tools for Model Checking", Joost-Pieter Katoen. In particular I ...
2
votes
1answer
606 views

CTL vs LTL - when a formula satisfy a model

I'm trying to understand the difference between LTL and CTL. In particular, i'm trying to understand when a model (a transition system eg. Kripke structure) satisfy a formula. This is my point of view:...
0
votes
1answer
119 views

Defining a new operator in CTL

Lets consider a new operator $B$ where $a B b$ means "in every execution, if $b$ holds some time, then $a$ does so before it" and we're asked to define it in CTL. My working: the system can only ...
0
votes
1answer
369 views

Given this transition system, for which states are these (very basic) LTL formulas fulfilled?

I missed a lot of lectures for this module due to surgery so I'm trying to teach it to myself now. This is the question I've been working on: First of all, would I be correct in saying that the LTL ...
2
votes
1answer
821 views

Proving Linear Time Temporal Logic formula □ ◊ f ⇔ ◊ □ f

I am new to this topic, Linear Time Temporal Logic and I am trying to prove this equivalence -- $\Box\Diamond f \Leftrightarrow \Diamond\Box f$ This is my take -- Basic definitions: $(\sigma, j) \...
0
votes
1answer
276 views

Difference between equivalence and implication

In terms of CTL formulae, what is the difference between equivalence and implication? (prop = some proposition, && = conjunction, AG = CTL syntax for "globally holds") E.g. AG (prop1 &&...
1
vote
1answer
151 views

Determining set of states that satisfy a CTL formulae

I'm trying to understand CTL formulae, and until now I've understood everything (or at least I thought I did). I have the following Kripke strucure: Now given the following CTL formulae ...
1
vote
1answer
85 views

Until quantifier of Computation Tree Logic

It's quite a short question: Refering to this Wikipedia article p U q means, that p has to hold at least until at some point <...
1
vote
1answer
415 views

Computation tree logic and Kripke structures

Specifications in Kripke structures are verified by Computation tree logic (CTL). However, refering to this Wikipedia article the CTL-operators are relative to a current state. So, when we want to ...
1
vote
2answers
126 views

Computation Tree Logic and its Temporal Opeators

I've got some questions about the temporal operators in computation tree logic: Does the Finally path-specific quantifier Fq ...