# Tag Info

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
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
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
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

• 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