# Questions tagged [model-checking]

The tag has no usage guidance.

49 questions
Filter by
Sorted by
Tagged with
55 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 ...
50 views

1 vote
75 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 ...
171 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$ ...
172 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 ...
144 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
1k 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
169 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 ... 59 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 ...
481 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
85 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 ...
149 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 ...
191 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, ...
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 vote
70 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 ...
144 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 ...
115 views

185 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.
124 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
488 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 ...
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$-...
542 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 ...
381 views

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

In , 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 ...
2k views

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$, ...
866 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 ...
17k 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.
819 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 ...
231 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. ...
583 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 ...
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 "...
660 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 ...
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 \$...