# Tag Info

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 ...

### 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 ...
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 ...
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 ...
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 ...
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 ...

### 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

### 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 ...
Accepted

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 ...
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 ...
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 ...
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)'$.
1 vote

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

Just learned about Bunched Logic which seems to fit the bill too.
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 ...
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 ...
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 ...
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 ...
1 vote
Accepted

### Counterexample for LTL - CTL equivalence

Consider the following model: you have 3 states, $s_0,s_1,s_2$ with the transitions: $s_0\to s_0$, $s_0\to s_1$, $s_1\to s_2$ and $s_2\to s_2$ and the labels are $L(s_0)=\{p,q\}$, $L(s_1)=\emptyset$ ...

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