The model-checking tag has no wiki summary.
-1
votes
1answer
45 views
Constructing automata with the same traces, but where a CTL-formula is not equally satisfied
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 ...
0
votes
1answer
114 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 ...
8
votes
1answer
188 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 ...
5
votes
1answer
107 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 ...
3
votes
2answers
200 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 ...
-3
votes
2answers
260 views
Kripke model and LTL vs CTL formulae interpretation [closed]
I have this Kripke model $M$:
$$
\begin{array}{ccccccc}
\to & (p, q) & \to & (\neg p, \neg q) & \to & (p, \neg q) \\
& \circlearrowright & & & & ...
9
votes
2answers
296 views
Expressiveness of Büchi vs CTL(*)
What is the relationship between the expressiveness of LTL, Büchi/QPTL, CTL and CTL*?
Can you give some references that cover as many of these temporal logics as possible (especially between linear- ...
-2
votes
2answers
134 views
Model checking Paxos
I have implemented consensus algorithm (based on Paxos). I have added some random test cases and it seems fine. To be sure, I want to do testing via model checking. I couldn't find a correct article ...
6
votes
1answer
106 views
When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?
A few papers I've been reading have algorithms on using interpolants for the following clauses (bounded model checking):
$$ \begin{align*}
A &= I \wedge T_1 \\
B &= T_2 \wedge T_3 \wedge ...
8
votes
2answers
241 views
Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)
I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, ...
1
vote
2answers
418 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 ...
5
votes
2answers
2k views
What is the difference between LTL and CTL?
I already read examples of formulas in CTL but not in LTL and vice-versa, but I'm having trouble gaining a mental grasp on LTL formulas and really what, at the heart, is the difference.
9
votes
6answers
602 views
A data structure for sets of trees.
Tries allow for efficient storage of lists of elements. The prefixes are shared so it is space efficient.
I am looking for a similar way to efficiently store trees. I would like to be able to check ...
6
votes
1answer
199 views
Papers on applying CTL over LTSs
Normally model checking with specifications written in CTL*/CTL is done over Kripke structures, however there are ways of doing it over somehow simpler Labelled Transition Systems, for instance ACTL. ...
6
votes
2answers
236 views
What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?
I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation.
For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want ...
15
votes
2answers
826 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 ...
12
votes
6answers
457 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 ...
5
votes
1answer
277 views
What is the parameterized complexity of following model checking problem?
Input: Graph $G$ and formula $\varphi_1(\vec x),\varphi_2(\vec x)$
Parameter: $tw(G)+|\varphi_1|+|\varphi_2|$
Problem: Decide if $|\varphi_1(G)|=|\varphi_2(G)|$
where $tw(G)$ is the treewidth ...
10
votes
1answer
208 views
Can someone suggest a recent survey on product form Markov chains?
I'm especially interested in their use in model checking applications. I have Open, Closed and Mixed Networks of Queues with Different Classes of Customers by Baskett et al. Any other suggestions ...
