Questions tagged [model-checking]
The model-checking tag has no usage guidance, but it has a tag wiki.
52
questions
1
vote
0
answers
51
views
Is this proof for completeness of regular model checking correct?
In "Calculational Design of A Regular Model Checker by Abstract Interpretation" by Patrick Cousot (link), on page 15 it can be seen that to prove the completeness of regular model checking (...
- 13
0
votes
0
answers
62
views
Number of quantifier alternations in prenex form of a formula
I'm currently studying hyperlogics and in particular HyperLTL/CTL*.
In model checking algorithms for such logics the number of quantifier alternations appearing in a formula can play an important role ...
0
votes
1
answer
65
views
Resources for first-order and second-order monadic logics with a model-checking objective
What are some good books and surveys for learning about first-order logic and monadic second-order logic?
I'm a graduate student in computer science with a focus on algorithms. For model-checking on ...
- 45
0
votes
1
answer
96
views
What is "structural model checking"?
In "Calculational Desing of a Regular Model Checker by Abstract Interpretation" (see) Cousot first defines a definition of model checking in his new settings at the page 9 then at the page ...
- 13
2
votes
0
answers
82
views
From formal models to programs - Model Checking
I am reading on Automata, Model Checking and CTL/LTL. I am looking for examples/references/books that help me understand the following:
Given a program (for example Python or Java), how can I change ...
- 59
6
votes
1
answer
257
views
What is the impact of encodings of sparse structures on the complexity of the model checking problem?
Some preliminaries first.
Consider a purely-relational structure (a.k.a. database) $\mathfrak{A} = (A, R_1^{\mathfrak{A}}, \ldots, R_{|\tau|}^{\mathfrak{A}})$ over some finite signature $\tau = \{ R_1,...
- 1,185
1
vote
1
answer
91
views
Is every countable, finite-branching LTS bisimilar to a tree?
Let $L$ be a finite set of labels, and let $\mathcal{C}$ be the set of finitely-branching transition systems labeled by $L$ and with a countable set of states. Let $\sim$ denote the bisimulation ...
2
votes
1
answer
235
views
Is modal $\mu$-calculus "equivalent" to bisimulation?
I know that propositional modal $\mu$-calculus $L\mu$ is bisimulation-invariant. However, I'm curious to what degree it captures bisimulation.
Q1: Given two labeled transition systems $T_1$, $T_2$ ...
0
votes
1
answer
266
views
Automatic theorem prover for first-order logic versus model checker
What's the formal difference between a model checker, and an automated theorem prover for first-order logic, i.e. something like Meson/Metis/Sledgehammer/Vampire/E? Link to a clear discussion of the ...
- 890
6
votes
1
answer
156
views
SMT solving with less-than theory and monotonic functions
I am attempting to solve a less-than theory within an SMT paradigm that involves variables assigned to reals and assumes that all the functions used in the theory are monotonic. The theory's signature ...
- 69
1
vote
1
answer
2k
views
Difference between CTMC, DTMC, and MDP
I've been reading the Handbook of Model Checking recently; I'm especially interested in probabilistic model checking, so have been led to the PRISM model checker. For background, I am very familiar ...
- 151
1
vote
1
answer
189
views
How are safety/liveness languages defined on the set of finite or infinite words?
Let $Σ$ be an alphabet (e.g., the powerset of atomic propositions coming from some Kripke structure, though such details are irrelevant here).
For infinite words, a language $P\subseteq Σ^ω$ is ...
user54864
0
votes
0
answers
69
views
Definition of MSO_1 for graph structures
What is the proper definition of MSO$_1$?
MSO$_1$ is also called the one-sorted MSO. In contrast, in MSO$_2$, the two-sorted MSO, first order variables and set variables are allowed to be of two ...
- 1,703
0
votes
1
answer
733
views
Are both safety and liveness properties closed under finite intersection?
Given two safety properties $P_1$ and $P_2$, is their intersection $P_1 \cap P_2$ also a safety property? Similarly, if $P_1$ and $P_2$ are liveness properties, is $P_1 \cap P_2$ also a liveness ...
- 125
1
vote
1
answer
89
views
Proving liveness-like property on an infinite tree
(Context: this is a problem from the middle of my dissertation work, abstracted into a more general problem. It's related to showing that some liveness properties hold, so perhaps work from something ...
8
votes
0
answers
158
views
Practical interactive proof schemes for NP-hard problems
Model-checking (in the sense of reachability in a succinct graph) is PSPACE-complete. SAT is NP-complete. Both problems are considered intractable, yet there exist tools capable of solving them on ...
- 1,122
0
votes
1
answer
201
views
What is "Effects" in Program Graph?
I have a doubt regarding the "effects" in Program Graph. Below is the image from the book Principle of Model Checking from Christel Baier and Joost-Pieter Katoen
(The MIT Press Cambridge, ...
- 1
0
votes
1
answer
47
views
How can theoretical modelling be converted into viable product? [closed]
Many a times modelling is just for the sake of modelling like exploring some properties of materials which does not help in converting the theoretical modelling into a viable product that can serve ...
- 1
1
vote
2
answers
73
views
Algorithms to synthesize optimal plans satisfying temporal logic constraints
I know how NuSMV can be applied on a model to check if certain temporal logic statements are satisfied, particularly LTL. I also know of the LTL to BA conversion routines available online.
I am ...
- 111
2
votes
2
answers
155
views
Practical example: how to formally verify "file name" implementation from a spec?
Say you have an OS-independent specification for file names. The file names are case sensitive, and let's say can't be more than 200 characters, and can't have : or ...
- 141
0
votes
0
answers
149
views
Approximating liveness properties with safety properties
Given a finite alphabet set $\Sigma$, the set $\Sigma^{\omega}$ of infinite words over $\Sigma$ can be topologized with a metric $d: \Sigma^{\omega} \rightarrow \mathbb{R}$ such as:
$\forall w_1, w_2 ...
- 163
1
vote
1
answer
714
views
Regular safety properties and bad prefixes of $\omega$-regular properties
I have two questions:
By starting with a nondeterministic Büchi automaton (NBA) $\mathcal{A}^{\varphi} = (Q, \Sigma, \rightarrow, I, F )$ for an $\omega$-regular property $\varphi$, we can construct ...
- 163
5
votes
2
answers
248
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 ...
-4
votes
1
answer
82
views
Probabilistic protocols [closed]
I want to model a probabilistic protocol using a model checker, but a lot of protocols are already implemented (e.g. Randomised Dining Philosophers, Dining cryptographers, Synchronous leader election ...
- 95
4
votes
1
answer
545
views
Decidability of membership in the fixed point of a rational relation
Given a finite alphabet $\Sigma$, a non-deterministic finite-state transducer representing rational a relation $T \subseteq \wp(\Sigma^* \times \Sigma^*)$, a finite state machine representing a ...
- 143
-4
votes
1
answer
162
views
Temporal Logic - Until [closed]
I have a doubt, in Linear Temporal Logic LTL, does the Until operator require that the first occurrence is the first term of the formula?
ex: a U b does require ...
- 131
0
votes
0
answers
98
views
Hoare program correctness
Which is the easiest way to find a valid Invariant for a While Program in the Hoare program correctness verification?
Is there a "guided" way to do that?
- 131
1
vote
2
answers
3k
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:
...
- 131
2
votes
1
answer
394
views
What is the space complexity of CTL model checking?
What is the space complexity of the CTL model checking algorithm via labeling without fairness (see e.g. Model Checking by Clarke at al Section 4.1 or Principles of Model Checking by Baier et al ...
5
votes
1
answer
122
views
Logics for timed resource control
I'm studying proof theory and I've seen that linear logic can be used as a way to control resource usage, since by the propositions-as-types it is equivalent to the linear lambda calculus.
Is there a ...
- 295
3
votes
2
answers
148
views
Typechecking liveness properties of coprograms
Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input.
I am ...
6
votes
1
answer
269
views
Is infinitary logic a logic in the sense of Gurevich?
Gurevich provides an exact definition of what Logic capturing PTIME is.
An abstract logic $L$ consists of
a set of $L[\tau]$-sentences for each vocabulary $\tau$,
and a mapping that maps a property $...
- 513
0
votes
0
answers
187
views
Given a CSL formula, how can we generate an automaton that accepts the formula?
The problem is same as the title, given a Continous Stochastic Logic(CSL) formula how can we create a machine which accepts the formula? Any intuitive ideas or references will be appreciated.
- 1
-1
votes
1
answer
128
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 ...
1
vote
1
answer
531
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 ...
9
votes
1
answer
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$-...
- 111
5
votes
1
answer
569
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 ...
- 153
4
votes
2
answers
387
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
votes
2
answers
2k
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 & & & & \...
- 119
12
votes
2
answers
1k
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
2
answers
338
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 ...
- 117
6
votes
1
answer
163
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
2
answers
286
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$, ...
- 241
2
votes
2
answers
901
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
2
answers
19k
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.
- 421
10
votes
6
answers
832
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 ...
- 803
6
votes
1
answer
246
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. ...
- 163
8
votes
2
answers
602
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 ...
- 8,861
17
votes
2
answers
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 "...
- 173
14
votes
6
answers
675
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 ...
- 241