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 ...
- 1,347
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 ...
- 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 ...
- 1,099
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 ...
- 8,923
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 $\...
- 8,923
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 ...
- 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.
...
- 5,616
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 ...
- 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 ...
- 854
1
vote
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 ...
- 8,923
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.
- 1,332
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 ...
- 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. ...
- 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).
- 376
Only top scored, non community-wiki answers of a minimum length are eligible