We’re rewarding the question askers & reputations are being recalculated! Read more.

Questions tagged [model-checking]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
5
votes
1answer
92 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 ...
1
vote
1answer
70 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 ...
1
vote
1answer
118 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 ...
0
votes
0answers
38 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 ...
0
votes
1answer
145 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 ...
1
vote
1answer
76 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
0answers
131 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
vote
2answers
58 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 ...
12
votes
2answers
12k 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.
0
votes
1answer
155 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, ...
0
votes
1answer
45 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 ...
2
votes
2answers
134 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 ...
1
vote
1answer
535 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 ...
0
votes
0answers
102 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 ...
5
votes
2answers
216 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
1answer
64 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 ...
4
votes
1answer
450 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 ...
-4
votes
1answer
87 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 ...
1
vote
2answers
2k 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: ...
0
votes
0answers
95 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?
5
votes
1answer
117 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 ...
2
votes
1answer
230 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 ...
3
votes
2answers
118 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
1answer
190 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 $...
0
votes
0answers
133 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.
-2
votes
2answers
286 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 ...
13
votes
6answers
607 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 ...
-1
votes
1answer
105 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 ...
5
votes
1answer
448 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 ...
1
vote
1answer
403 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
1answer
964 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$-...
12
votes
2answers
718 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- ...
-1
votes
2answers
1k 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 & & & & \...
4
votes
2answers
318 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 ...
6
votes
1answer
148 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
273 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$, ...
2
votes
2answers
765 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 ...
10
votes
6answers
776 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 ...
8
votes
2answers
482 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 ...
6
votes
1answer
220 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. ...
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 "...
5
votes
1answer
307 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 of $...
11
votes
1answer
238 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 ...