5 votes

Linear Temporal Logic (LTL) Syntax Infinitely Often

Consider just $Fx$. It means that at some point in time, say $t_k$, from the perspective of current moment $t_0$, $x$ will be true. After this moment, $x$ may never again be true. Specificaly, at the ...
Sandro Lovnički's user avatar
5 votes
Accepted

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

In order to prove the equivalence of two formulas $\phi,\psi$, it is enough to show that for every computation $\pi$, it holds that $\pi\models \phi$ iff $\pi\models \psi$. This is semantic ...
Shaull's user avatar
  • 17.2k
4 votes
Accepted

CTL* query evaluation order

Your interpretation of the $G$ modality is incorrect; it does not inherently talk about all paths. In particular, the example you give specifies that there is a path such that from some point on, all ...
Klaus Draeger's user avatar
4 votes

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

\begin{alignat*}{2} \Box \varphi \to \Diamond q &\equiv \neg \Box \varphi \lor \Diamond \psi &&\text{($\to$ elim)}\\ &\equiv \Diamond \neg \varphi \lor \Diamond \psi &&\text{(...
user3121260's user avatar
4 votes
Accepted

What's the definition of ACTL?

ACTL is the universal fragment of CTL. Thus, existential path quantification is not allowed. So a path formula is of the form $AF\psi$, $AG\psi$, or $AX\psi$ (or a conjunction or disjunction of path ...
Shaull's user avatar
  • 17.2k
4 votes
Accepted

What are the differences between propositional logic and temporal logic?

An interpretation in propositional logic consists of assigning a truth value to every variable. In contrast an interpretation of, say, LTL consists of assigning a truth value to every variable at each ...
Yuval Filmus's user avatar
4 votes
Accepted

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

You can learn a lot about CTL at Wikipedia page. The sentence you need to write, expressed more closely in the vocabulary of CTL operators, would be Along all paths starting from current state, it ...
Sandro Lovnički's user avatar
3 votes
Accepted

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

(This is the "standard" example which proves that CTL is not a superset of LTL, in terms of expressiveness) Consider this system: state $q0$, transitions to $q0$ and $q1$ state $q1$, transition to $...
chi's user avatar
  • 14.6k
3 votes
Accepted

Difference between CTL and CTL*

First, let's see a formula that's in CTL$^*$ but not in CTL: $EGFp$. That is, there exists a path with infinitely many $p$'s. One intuition (and this is by no means a formal argument) is that the &...
Shaull's user avatar
  • 17.2k
3 votes
Accepted

Temporal logic - mixing AF and AG in CTL formula

Does it mean that: 1. or 2. or 3.? Your second interpretation is correct: $\varphi_1 \rightarrow AG(\varphi_2)$ is a CTL state formula, and to check whether it is satisfied by a state $s$, the path ...
f9c69e9781fa194211448473495534's user avatar
2 votes

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

I would interpret your problem as follows: Given a non-deterministic Büchi automaton representing some language $L$, you want to enumerate all shortest good prefixes of $L$ such that in every ...
DCTLib's user avatar
  • 2,742
2 votes
Accepted

Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$

If you're just asking for any model satisfying the formula, you simply try to make one of these the case The left hand side false The right hand side true Let's just pick number 2. You have to make ...
Pål GD's user avatar
  • 16.1k
2 votes
Accepted

Given LTL formulas $m$ and $p$, is there a tool that can check whether $m \models p$ does hold?

Yes, you can use an LTL-to-Büchi-automaton translator for this. Let's assume that you want to check if $\psi \rightarrow \psi'$ is a valid LTL formula, i.e., every word satisfying the LTL property $\...
DCTLib's user avatar
  • 2,742
2 votes
Accepted

LTL globally implies

You seem to be pretty confused, so let's sort some things out. First, it's "implies", not "replies". That is, the formula $\phi\implies \psi$ means that if $\phi$ holds, then $\psi$ holds. To be more ...
Shaull's user avatar
  • 17.2k
1 vote

Logics for multi-agent and distributed systems and algorithms

TLA+ is commonly used for verification of distributed algorithms. I've seen it actively used by researchers and industry engineers/architects.
Valentin Kuznetsov's user avatar
1 vote

What is the Kripke semantic for a linear temporal logic?

tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind. Details: Let $P$ be a set of atomic proposition. Write $\Sigma$ for $P$'s powerset. Write $T$ for ...
Kai's user avatar
  • 865
1 vote
Accepted

Which temporal logic is the one described in Manna & Pnueli's "The Temporal Logic of Reactive and Concurrent Systems: Specification"?

LTL. PS The very book you mention has a historical note section discussing various other temporal logics near page 271. Edit (leaving the above intact for the comments to make sense): None of the ...
Kai's user avatar
  • 865
1 vote

Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$

General notes on LTL Intuitively, LTL formulas are statements about infinite sequences (or "infinite words"). First, you have to understand what these sequences consist of. In the usual definition ...
f9c69e9781fa194211448473495534's user avatar
1 vote
Accepted

Prove that $\text{EF p}$ can't be written in LTL

There is a delicate point here, about the semantics of LTL vs CTL. Given a formula $\psi$ in LTL, we say that it holds in a structure $K$ if every path in $K$ satisfies $\psi$. In CTL, however, the ...
Shaull's user avatar
  • 17.2k
1 vote

LTL Logic Finally, Globally and Until to irreflexive Version

Sorry, I misread your question at first as wanting to express the irreflexive variant using the reflexive variant (which could be done with the next operator). You don't actually need the next for the ...
f9c69e9781fa194211448473495534's user avatar
1 vote

Semantics of E and A operators in CTL*

I believe it means that $\sigma,\sigma$ should share the same prefix up to position $i$. Then the quantification ranges over all possible extensions of this prefix from state $\sigma(i) = \sigma(i)'$.
SimonJ's user avatar
  • 134
1 vote

Reasoning about resources: "resource logics"?

Just learned about Bunched Logic which seems to fit the bill too.
Lance's user avatar
  • 2,223
1 vote

Reasoning about resources: "resource logics"?

Do you mean a resource-aware logic? If so, yes, there's linear logic [Girard, 1987] (as was already noted in the comments). It has had a big influence on the study of concurrency and implicit ...
fmontesi's user avatar
  • 171
1 vote

Linear Temporal Logic, Idempotent law

Also by definition of $G$, some formula holds in every state. Well, $\sf true$ holds in every state. I'm unsure about why you mention $G$ here. So if globally $\phi$ holds until we see $\psi$ does ...
chi's user avatar
  • 14.6k
1 vote

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

This is a hot topic at the moment. Read this recent paper by Judea Pearl for example. In general, ML and AI are not very good at causal inference at the moment, because it requires a symbolic ...
quant_dev's user avatar
  • 111
1 vote

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

Consider a system with 3 states, $s_1,s_2,s_3$ and the following transitions: $s_1\to s_1$, $s_1\to s_2$, $s_2\to s_3$ and $s_3\to s_3$. The state $s_2$ is labelled $p$. Clearly $E[GF p]$ doesn't ...
Shaull's user avatar
  • 17.2k

Only top scored, non community-wiki answers of a minimum length are eligible