Model checking and model synthesisfrom partial models: a logic-based perspective

TL;DR

This paper explores logical and algorithmic challenges in verifying and synthesizing full models from partial system representations, focusing on modal and temporal logics, and proposes a tableaux-style solution for several logics.

Contribution

It introduces a unified framework for model checking and synthesis from partial models and outlines a tableaux-based procedure for modal and temporal logics.

Findings

Proposes a general tableaux-style procedure for model synthesis.

Addresses both model checking and synthesis problems.

Applies to modal and temporal logics like K, LTL, CTL, ATL.

Abstract

I consider the following generic scenario: an abstract model M of some 'real' system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in some logical language. This scenario has at least two essentially different interpretations, leading to two, essentially different, formal logical and algorithmic problems: "Model Synthesis from Partial Models", where some 'admissible' extension of M to a full model must satisfy the specification, and "Model Checking of Partial Models", where all 'admissible' extensions of M to a full model must satisfy the specification. These problems naturally extend the classical logical decision problems of Satisfiability, Validity, and Model Checking. Here I briefly discuss both problems in the contexts of classical, modal and temporal logics. I make some observations, state some open questions, and outline a general tableaux-style procedure that solves the problem of unconstrained model synthesis from finite partial models for several well-known modal and temporal logics, incl. K, LTL, CTL, ATL.