Questions tagged [linear-temporal-logic]

LTL (linear temporal logic or linear-time temporal logic) is a temporal logic that can encode assertions about the future of traces.

19 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
13 votes
1 answer

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 ...
User's user avatar
  • 411
4 votes
0 answers

Understanding a proof from a paper (model checking game)

I'm reading the paper: "Model Checking Games for Branching Time Logics" by Martin Lange and Colin Stirling - The ...
Mcgfbtl's user avatar
  • 41
3 votes
0 answers

Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
reinierpost's user avatar
  • 5,359
2 votes
0 answers

Does Rice's theorem apply to sequential logic circuits?

I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any ...
Grisu47's user avatar
  • 121
2 votes
0 answers

Equivalence preserving operator from CTL* to LTL

The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
tender hopper's user avatar
2 votes
0 answers

Satisfying of $\square (\neg A \cup B)$

Let's consider the following formula: $\square (\neg A \cup B)$. Does the following computation satisfy it? The numbers in brackets are number of state. (0) $\neg A, \neg B$ (1) $\neg A, B$ (2) $...
user avatar
2 votes
0 answers

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
TomR's user avatar
  • 1,381
1 vote
0 answers

About next operator duality in LTL

I'm learning LTL (linear temporal logic) and we learned that a model $M$ and a starting position $q_0$ satisfies a LTL formula $\psi$ iff for every path $\pi$ starting at $q_0$ it is true that $\pi \...
Golden's user avatar
  • 111
1 vote
0 answers

Errors in examples of Vardi's paper "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces"

The paper Linear Temporal Logic and Linear Dynamic Logic on Finite Traces has the following examples on page 4: Q1. (Update to Q1: solved. See the comment by DCTLib.) The first example says that the ...
Ayrat's user avatar
  • 1,045
1 vote
1 answer

Translating Natural Language to LTL Formulae

I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct. I'm given the sentences, and my assumption is that $l$ ...
UnevenMango's user avatar
1 vote
1 answer

What does “linear” in Linear Temporal Logic refer to?

Consider the term linear temporal logic (in the meaning of linear-time temporal logic). In linear temporal logic, what does linear refer to: to temporal or to logic? If I interpret http://en....
user avatar
1 vote
0 answers

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 ...
LTL's user avatar
  • 11
1 vote
0 answers

generic technique to build LTL/CTL formula that satisfy specific inputs to a model

I have an automaton, for example the below automaton and would like to generate a single formula (LTL or CTL, or some other representation) that satisfy exactly the traces provided. e.g., $t_1 = i^*...
Zack Newsham's user avatar
1 vote
0 answers

Size of parity automata and Buchi automata from linear time mu-calculus?

Given a linear time mu-calculus formula, there are many works on transforming the formula to Buchi or Parity automaton. Using the best algorithm, what is the size of the resulting Buchi automaton and ...
crazybird's user avatar
0 votes
0 answers

Is first order linear temporal logic a special case of first order modal logic?

Propositional linear temporal logic is a special case of propositional modal logic. Is first order linear temporal logic likewise a special case of first order modal logic?
Evan Aad's user avatar
  • 227
0 votes
0 answers

Can an LTL formula uniquely be represented by an expression tree?

Just like we can represent a mathematical expression uniquely with a binary expression tree, I was wondering if we could do the same for LTL formulae? Such that no two different looking LTL formula ...
user3598542's user avatar
0 votes
0 answers

How to draw a Non Deterministic Buchi Automaton (NBA) from the given property?

I'm new to LTL and Buchi automaton, and I have a hard time in constructing NBA from the given formula or the property. Could somebody please help me? The following property is given, P= "Whenever ...
Rao208's user avatar
  • 1
0 votes
0 answers

Show the formula is a law of LTL

Show that the following formula is a law of LTL, i. e. the formula is satisfied on all paths in all models G(p → X q) ∧ G(q → F p) ∧ p → G F p I dont know how ...
Zeist's user avatar
  • 173
-1 votes
0 answers

Validity of ♢(p ∨ q) → ¬□(¬p ∨ ¬q) in linear temporal logic

Let p, q denote propositional variables and ϕ, ψ denote LTL formulas. Is the following LTL formulas is valid? ♢(p ∨ q) → ¬□(¬p ∨ ¬q) and how to proof using A not satisfying word is σ1,unsat := {p}∅∅......
sunshine's user avatar