# Questions tagged [model-checking]

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

55 questions
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 ...
• 181
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 ...
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 ...
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 (...
• 13
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 ...
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 ...
• 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 ...
• 13
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 ...
6 votes
1 answer
262 views

• 163
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 ...
• 163
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 ...
-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 ...
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 ...
-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 ...
• 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
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: ...
• 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 ...
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 ...
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 ...
6 votes
1 answer
272 views

• 241
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.
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 ...
• 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. ...
• 163