Modal symbolic learning is the subfield of artificial intelligence that brings together machine learning and modal logic to design algorithms that extract modal logic theories from data. The generalization of model checking to multi-models and multi-formulas is key for the entire inductive process (with modal logics). We investigate such generalization by, first, pointing out the need for finite model checking in automatic inductive reasoning, and, then, showing how to eficiently solve it. We release an open-source implementation of our simulations.
the finite state space of the system to assess whether some specification (i.e., property of the system) is true or not.
In this work, we argue that model checking plays a crucial role in the induction of modal formulas, and that an eficient model checking algorithm is essential for modal symbolic learning methods. We show how to extend the typical model checking machinery to check multiple formulas on multiple models, and experimentally show how memoization (i.e. storing model checking results for later reuse) can be leveraged to drastically reduce model checking computational time. Finally, we release an open-source implementation to reproduce the experiments of this work.
modal logic (ML) are obtained by the following grammar: Given a set of propositional letters as the alphabet, the well-formed formulas of the propositional
::= | ¬ | ∨ | ♢ , and call the height of a formula the height of its syntax tree. where the remaining classic Boolean operators can be obtained as shortcuts. In what follows, we use □ to denote ¬♢ ¬ . The modality ♢ (resp., □ ) is usually referred to as it is possible that (resp., it is necessary that). We refer to ℱ as the set of formulas produced by the above grammar,
ML is paradigmatic of temporal, spatial, and spatio-temporal logics, and it is an extension of propositional logic (PL). Its semantics is given in terms of Kripke models. A Kripke model = (, , ) is a Kripke frame (, ) composed by a non-empty (possible infinite, but countable) set of worlds (which contains a distinguished world 0, called initial world), a binary accessibility relation ⊆ ×
, and a valuation function : → 2 , which associates each world with the set of propositional letters that are true on it. The truth relation , ⊩ , for a generic (Kripke) model , a world (in that model), and a formula (to be interpreted on that model), is given by the following clauses: , ⊩ , ⊩ ¬
, ⊩ ♢
, ⊩ 1 ∨ 2 if
if
if
if
, ⊩ 1 or , ⊩ 2;
∃′ s.t. ′ and , ′ ⊩ .
∈ ();
, ⊮ (i.e., it is not the case that , ⊩ );
In the following, we use ⊩ to denote , 0 ⊩ . In modal symbolic learning, Kripke
models can be used to represent data such as time series, images, audio, videos, and graphs,
which, in the era of big data, accounts for 80% − 95% of the existing data [
Among the many interesting mathematical problems studied over the years in the field of ML
there is model checking [
In real-world contexts, it is common to check many formulas on many Kripke models. In fact, modal symbolic learning is an inductive statistical process, that learns a general theory, seen as multiple ML formulas, from datasets of Kripke models. This sets the stage for the more general problem of finite model checking of multiple models against multiple formulas. Let = {1, . . . , } be a collection of Kripke models and Φ = { 1, . . . , } be a collection of ML formulas, then the multi-models and multi-formulas finite model checking problem is the problem of deciding, for all ∈ and for all ∈ Φ, if ⊩ . The straightforward approach involves calling the single model checking procedure · times; however, the memoization results generated by a single call can be reused for a later call on the same model. In fact, the memoization structure for a single model can be shared for checking all formulas; ideally, this reduces the overall computational load, but it requires more memory accesses which, in turn, introduce overhead. This tradeof can be mitigated by only sharing memoized (sub)formulas with height no greater than a fixed parameter ℎℎ, leveraging the fact that shorter (sub)formulas are more likely to be checked in the future.
We prove and quantify the benefits of a shared memoization structure in an experimental
setting. The Kripke models are generated by fixing the same Kripke frame with 20 worlds,
randomly generated using the Fan-in/Fan-out method from [
The cumulative times of the diferent approaches are illustrated in Fig. 1. It can be observed that sharing at least the propositional letters is beneficial in all cases; in other words, the shared memoization approach improves over the non-shared one. When comparing diferent 0.6 ) ( e itm0.4 e v i t la0.2 u m u C0.0 ) (6 e m i te4 v i t a lu2 m u C 0 non-shared ℎℎ = 0 ℎℎ = 1 400 600 -th formula (a) ℎ = 1 non-shared ℎℎ = 0 ℎℎ = 1 ℎℎ = 2 ℎℎ = 4 2000 -th formula (c) ℎ = 4 parametrizations of the shared approach, it appears that, within the given experimental setting, ℎℎ = 1 and ℎℎ = 2 tend to improve over the other values. Overall, the speedup achieved by shared memoization, calculated as the ratio between the total cumulative times of the non-shared and best shared approaches, ranges from 185% to 471%. The open-source implementation of our experiments, together with more results revealing similar trends, is available at https://github.com/aclai-lab/OVERLAY2022.jl.
In this work, we considered modal logic as paradigmatic of temporal, spatial, and spatiotemporal logics, and noted how Kripke models can be used for representing data with no predefined structure (which, nowadays, amounts to the vast majority of data). We pointed out the importance of finite model checking in automatic inductive reasoning. We generalized this problem to a multiple models and multiple formulas setting, showing the benefits of a shared memoization approach. This study is part of a bigger investigation on modal symbolic learning, which attempts at learning qualitative patterns from unstructured objects, seen as Kripke models, which is not possible with the limited expressive power of propositional logic.