# Tagged Questions

The tag has no usage guidance.

37 views

### Complexity of propositional LTL with past operators and freeze quantifier?

In "A Really Temporal Logic", by R.Alur and A.Henziger, they introduce an extension of Linear Temporal Logic with a freeze quantifier $x.\phi$, which allows to "give a name" to the current time point ...
53 views

### Global satisfiability in LTL

In propositional linear temporal logic (LTL) over $\mathbb{N}$, it is decidable whether a formula $\varphi$ is satisfiable from time point 0. Is it known to be un/decidable to check the ...
144 views

### Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso?

Are there linear time temporal logics that can express some property $P_{nonlasso}$ that does have a counterexample, but none that is a lasso (or finite)? Details: One advantage of model checking ...
124 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)\\ ...
354 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.
396 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: ...
375 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 ...
104 views

### What is the difference between LTL connectives X and O?

I have seen two different sets of connectives for LTL (see the picture): I have learned LTL by the connectives of the first column ($X, F, G,$ ...). The table (from Wikipedia) says that the ...
139 views

### Resource for LTL formulae?

I would like to practice on some problems for using LTL formulae but besides the foundations and theory there are only every few examples. I know that having understood theory is not enough. Where can ...
90 views

### Constructing automata with the same traces, but where a CTL-formula is not equally satisfied [closed]

Hard to put this question in a short title. As part of a self-exercise, I'm trying to solve 6.15b of Principles of Model Checking by Baier and Katoen. You're supposed to prove that there does not ...
226 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 ...
252 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 ...
210 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 ...
93 views

### Temporal Logic and Access Control Models

What is the best way to describe the semantics of a new access control model?. I heard the temporal logic is the way to go. Is it true?
148 views

### Implicit Non-deterministic Buchi determinization

I am doing implicit Buchi determination for LTL logic in hardware where the combinational logic represents the set of states. But instead of using acceptance states, I am using final state (as in ...
239 views

### Problem in embedding

I want to embed PPTL(a kind of logic) in Coq. Because of its complex semantics, I just embed its systax. ...
254 views

### What is an unambiguous language in the sense of Schützenberger?

I'm reading Thomas Wilke's survey on the connections between Temporal Logic and finite automata, finite semigroups and first-order logic. In Theorem 6 (by Kamp), the fragment \$\mathrm{TL}[\mathsf{F},\...