Share Your Experience: Take the 2024 Developer Survey

# Tag Info

### 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 ...
• 1,191
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 ...
• 17.2k
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 ...
• 17.2k
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 ...
• 2,176

### 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{(...
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 ...
• 277k
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 ...
• 1,191
Accepted

• 2,787
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 ...
• 17.2k
1 vote
Accepted

### Given 2 Kripke structures M1 and M2, if there exists a simulation from M1 to M2 and a simulation from M2 to M1, is there a bisimulation from M1 to M2?

Yes your intuition is correct. The fact is that the 2 relations can be disjoint when considering just one-sided simulation relations but for bisimulation we need 1 relation with symmetry which is ...
• 64
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.
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 ...
• 908
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 ...
• 908
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 ...
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 ...
• 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 ...
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)'$.
• 134
1 vote

### Reasoning about resources: "resource logics"?

Just learned about Bunched Logic which seems to fit the bill too.
• 2,243
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 ...
• 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 ...
• 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 ...
• 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 ...
• 17.2k

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