Questions tagged [model-checking]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
17
votes
2answers
1k views

Trace Equivalence vs LTL Equivalence

I am looking for an easy example of two transition systems that are LTL equivalent, but not trace equivalent. I have read the proof of Trace Equivalence being finer than LTL Equivalence in the book "...
2
votes
2answers
835 views

Equivalence of two basic blocks

My questions: What are other names for this and similar problems and their fields? ("equivalence of varieties in universal algebra", "equivalence of algebraic structures", "rewriting systems for ...
14
votes
6answers
654 views

What are practically computable properties of Labelled Transition Systems?

I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would ...
9
votes
1answer
1k views

CTL* and mu-calculus

it is well known that the modal $\mu$-calculus is one of the most expressive temporal logics for expressing properties of trees/graphs, and that CTL* is strictly less expressive than the $\mu$-...
4
votes
2answers
376 views

Inductive definition of ECTL*: how are recursive formulas forbidden?

In [1], the extended computation tree logic ECTL* is inductively defined as the propositional formulas over all E($A(F_1,..F_n)$), where E is the existential path quantifier and $A$ some Büchi ...
1
vote
1answer
472 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 ...