Questions tagged [model-checking]

The tag has no usage guidance, but it has a tag wiki.

Filter by
Sorted by
Tagged with
1 vote
0 answers
64 views

Why is the model-checking problem for MSO $\textsf{PSPACE}$-complete?

I am currently reading "Parameterized Complexity Theory" by J. Flum and M. Grohe. In Chapter 10.3 they state in the first paragraph: Let us remind the reader that the model-checking problem ...
user11718766's user avatar
6 votes
0 answers
106 views

How to prove clock equivalence is a time-abstracted bisimulation

An important step of developing the theory of timed automata is to reduce the question of reachability in the timed automata, which has infinitely-many states, to the question of reachability in an ...
generic_logician's user avatar
2 votes
2 answers
77 views

State machine classes with sub-exponentially growing model spaces

State machines are useful tools for system modelling. They allow for a compact visual notation of discrete systems and provide a formal model of them. However, reasoning about the correctness of an ...
stateMachineOperator's user avatar
1 vote
0 answers
54 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 (...
Senmorta's user avatar
0 votes
0 answers
69 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 ...
timtombobjohn's user avatar
0 votes
1 answer
71 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 ...
fva's user avatar
  • 45
0 votes
1 answer
101 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 ...
Senmorta's user avatar
2 votes
0 answers
87 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 ...
Karl 17302's user avatar
6 votes
1 answer
262 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,...
Bartosz Bednarczyk's user avatar
1 vote
1 answer
94 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 ...
wanderingmathematician's user avatar
2 votes
1 answer
250 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$ ...
wanderingmathematician's user avatar
0 votes
1 answer
311 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 ...
Ilk's user avatar
  • 920
6 votes
1 answer
161 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 ...
C. Bowers's user avatar
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 ...
ahelwer's user avatar
  • 151
1 vote
1 answer
203 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 ...
user avatar
0 votes
0 answers
72 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 ...
Cyriac Antony's user avatar
1 vote
1 answer
845 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 ...
kauray's user avatar
  • 135
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 ...
Jonathan Schuster's user avatar
8 votes
0 answers
162 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 ...
David Monniaux's user avatar
0 votes
1 answer
203 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, ...
Rao208's user avatar
  • 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 ...
Shati's user avatar
  • 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 ...
user_1_1_1's user avatar
2 votes
2 answers
162 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 ...
Lance's user avatar
  • 141
0 votes
0 answers
151 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 ...
Ahmed Nassar's user avatar
1 vote
1 answer
737 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 ...
Ahmed Nassar's user avatar
5 votes
2 answers
261 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 ...
DaveBall aka user750378's user avatar
-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 ...
John Smith's user avatar
4 votes
1 answer
546 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 ...
Daniel Franke's user avatar
-4 votes
1 answer
176 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 ...
Nk SP's user avatar
  • 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?
Nk SP's user avatar
  • 131
1 vote
2 answers
4k 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: ...
Nk SP's user avatar
  • 131
2 votes
1 answer
404 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 ...
DaveBall aka user750378's user avatar
5 votes
1 answer
124 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 ...
Rodrigo Ribeiro's user avatar
3 votes
2 answers
155 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 ...
Carl Patenaude Poulin's user avatar
6 votes
1 answer
272 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 $...
Joachim's user avatar
  • 513
0 votes
0 answers
188 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.
Brainy's user avatar
  • 1
-1 votes
1 answer
129 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 ...
Bla Blaat's user avatar
1 vote
1 answer
571 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 ...
DaveBall aka user750378's user avatar
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$-...
LORE81's user avatar
  • 111
5 votes
1 answer
570 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 ...
walkmanyi's user avatar
  • 153
4 votes
2 answers
392 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 ...
DaveBall aka user750378's user avatar
-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 & & & & \...
dendini's user avatar
  • 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- ...
DaveBall aka user750378's user avatar
-2 votes
2 answers
343 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 ...
mohan's user avatar
  • 117
6 votes
1 answer
164 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 \...
Suhail Sherif's user avatar
8 votes
2 answers
288 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$, ...
Ahmed Masud's user avatar
2 votes
2 answers
912 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
20k 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.
Anonymous Coward's user avatar
10 votes
6 answers
842 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 ...
Abdallah's user avatar
  • 803
6 votes
1 answer
254 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. ...
Camilo's user avatar
  • 163