4 votes
Accepted

Resources for first-order and second-order monadic logics with a model-checking objective

It depends what precisely do you want to learn. A good reference is the finite model theory book by Libkin. https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf (chapters 2 and 7). If you want more ...
Bartosz Bednarczyk's user avatar
4 votes
Accepted

Are both safety and liveness properties closed under finite intersection?

Safety properties are closed under finite intersection. This can be seen by following Alpern and Schneider's characterisation which showed that safety properties are limit-closed when viewed ...
Kai's user avatar
  • 854
4 votes
Accepted

What is the impact of encodings of sparse structures on the complexity of the model checking problem?

I don't know of any natural logic, but the following is in any case a logic for which the combined complexity of the model-checking problem is different for matrix and list encodings. First, we know ...
Reijo Jaakkola's user avatar
3 votes
Accepted

Is every countable, finite-branching LTS bisimilar to a tree?

Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree. Q2: No, by a cardinality argument. For instance take infinite binary trees with $L=\{a,b\}$. Each tree has countable set of states ...
Denis's user avatar
  • 8,678
3 votes

Is modal $\mu$-calculus "equivalent" to bisimulation?

For Q1, the answer is yes if we consider image-finite systems: for all node $t$ and label $a$, the number of $a$-successors of $t$ must be finite. In this case you don't even need fixpoints of the $\...
Denis's user avatar
  • 8,678
3 votes
Accepted

Automatic theorem prover for first-order logic versus model checker

To add to the answer in the comments, it might help to first ask what the difference is between a model checker and an automated theorem prover for propositional logic. Given the statement $$p \wedge ...
selig's user avatar
  • 333
3 votes
Accepted

Difference between CTMC, DTMC, and MDP

The "probabilistic" element in probabilistic model checking is that the system being checked is probabilistic, not that we add probabilities to an existing deterministic or non-deterministic system. ...
Shaull's user avatar
  • 5,561
2 votes

State machine classes with sub-exponentially growing model spaces

I believe that there are no reasonable model where the number of machines grow subexponentially, in the sense that either such a model would be remarkably not expressive, or would require huge ...
Rémi's user avatar
  • 262
2 votes
Accepted

What is "structural model checking"?

I hadn't seen that term before either. In essence it seems to mean a model checking algorithm taking a program $P$ (with its syntactic structure) and a property that exploits $P$'s structure in the ...
Kai's user avatar
  • 854
2 votes

How are safety/liveness languages defined on the set of finite or infinite words?

The answer is yes to all questions, so it is enough to answer 2 and 4, as the definitions work in particular for languages of finite words: A language $P\subseteq \Sigma^*\cup\Sigma^\omega$ is safety ...
Denis's user avatar
  • 8,678
1 vote

SMT solving with less-than theory and monotonic functions

I can think of 2 straight forward approaches Directly add $\forall xy (x < y \Rightarrow f(x) < f(y))$. Or Akcermannize the problem and add these as axioms for all pairs of terms.
Mikolas's user avatar
  • 1,322
1 vote

What is "Effects" in Program Graph?

What you wrote is correct. The actions $\textit{coin}$ and $\textit{ret_coin}$ do not change the values of the variables $\textit{Var} = \{\textit{nsoda}, \textit{nbeer}\}$, i.e., the number of soda ...
tjanson's user avatar
  • 113
1 vote

How can theoretical modelling be converted into viable product?

I'm assuming that you're really asking, "how do I do something useful with modelling and theory." The easiest answer is to work in a modelling and simulation field that makes useful products. ...
ed kaye's user avatar
  • 11
1 vote

Algorithms to synthesize optimal plans satisfying temporal logic constraints

Maybe take a look at http://www.syntcomp.org/ This is a competition of tools solving the LTL synthesis problem (and some related problems).
Markus's user avatar
  • 366

Only top scored, non community-wiki answers of a minimum length are eligible