-
Weak Simplicial Bisimilarity and Minimisation for Polyhedral Model Checking
Authors:
Nick Bezhanishvili,
Laura Bussi,
Vincenzo Ciancia,
David Gabelaia,
Mamuka Jibladze,
Diego Latella,
Mieke Massink,
Erik P. de Vink
Abstract:
The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking…
▽ More
The work described in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking on polyhedral models using the logical language SLCS$η$, a weaker version of SLCS, where by ``weak'' we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. two points are weakly simplicial bisimilar if and only if they are logically equivalent for SLCS$η$. Similarly, two cells are weakly $\pm$-bisimilar if and only if they are logically equivalent in the poset-model interpretation of SLCS$η$. Furthermore we present a model minimisation procedure, and prove that it correctly computes the minimal model with respect to weak $\pm$-bisimilarity, i.e. with respect to logical equivalence of SLCS$η$. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.
△ Less
Submitted 6 June, 2025; v1 submitted 18 November, 2024;
originally announced November 2024.
-
Weak Simplicial Bisimilarity for Polyhedral Models and SLCS_eta -- Extended Version
Authors:
Nick Bezhanishvili,
Vincenzo Ciancia,
David Gabelaia,
Mamuka Jibladze,
Diego Latella,
Mieke Massink,
Erik P. de Vink
Abstract:
In the context of spatial logics and spatial model checking for polyhedral models -- mathematical basis for visualisations in continuous space -- we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of $\pm$-bisimilarity on cell-poset models, a discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff…
▽ More
In the context of spatial logics and spatial model checking for polyhedral models -- mathematical basis for visualisations in continuous space -- we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of $\pm$-bisimilarity on cell-poset models, a discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their repesentations are weakly $\pm$-bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral models, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCS_eta, a weaker version of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS_eta. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS_eta. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.
△ Less
Submitted 9 April, 2024;
originally announced April 2024.
-
On Bisimilarity for Quasi-discrete Closure Spaces
Authors:
Vincenzo Ciancia,
Diego Latella,
Mieke Massink,
Erik P. de Vink
Abstract:
Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighborhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bi…
▽ More
Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighborhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bisimilarity that are logically characterised by corresponding modal logics with spatial modalities: (i) CM-bisimilarity for closure models (CMs) is shown to generalise topo-bisimilarity for topological models and to be an instantiation of neighbourhood bisimilarity, when CMs are seen as (augmented) neighbourhood models. CM-bisimilarity corresponds to equivalence with respect to the infinitary modal logic IML that includes the modality ${\cal N}$ for ``being near to''. (ii) CMC-bisimilarity, with `CMC' standing for CM-bisimilarity with converse, refines CM-bisimilarity for quasi-discrete closure spaces, carriers of quasi-discrete closure models. Quasi-discrete closure models come equipped with two closure operators, Direct ${\cal C}$ and Converse ${\cal C}$, stemming from the binary relation underlying closure and its converse. CMC-bisimilarity, is captured by the infinitary modal logic IMLC including two modalities, Direct ${\cal N}$ and Converse ${\cal N}$, corresponding to the two closure operators. (iii) CoPa-bisimilarity on quasi-discrete closure models, which is weaker than CMC-bisimilarity, is based on the notion of compatible paths. The logical counterpart of CoPa-bisimilarity is the infinitary modal logic ICRL with modalities Direct $ζ$ and Converse $ζ$, whose semantics relies on forward and backward paths, respectively. It is shown that CoPa-bisimilarity for quasi-discrete closure models relates to divergence-blind stuttering equivalence for Kripke models.
△ Less
Submitted 7 July, 2025; v1 submitted 27 January, 2023;
originally announced January 2023.
-
Lowerbounds for Bisimulation by Partition Refinement
Authors:
Jan Friso Groote,
Jan Martens,
Erik. P. de Vink
Abstract:
We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $Ω((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$ and for parallel algorithms this is $Ω(n)$, where $n$ is the number of states and $m$ is the number of transitions. The lowerbounds are obtained by an…
▽ More
We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $Ω((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$ and for parallel algorithms this is $Ω(n)$, where $n$ is the number of states and $m$ is the number of transitions. The lowerbounds are obtained by analysing families of deterministic transition systems, ultimately with two actions in the sequential case, and one action for parallel algorithms. For deterministic transition systems with one action, bisimilarity can be decided sequentially with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that this approach is not of help to develop a faster generic algorithm for deciding bisimilarity. For parallel algorithms there is a similar situation where these techniques may be applied, too.
△ Less
Submitted 10 May, 2023; v1 submitted 14 March, 2022;
originally announced March 2022.
-
Towards a Feature mu-Calculus Targeting SPL Verification
Authors:
Maurice H. ter Beek,
Erik P. de Vink,
Tim A. C. Willemse
Abstract:
The modal mu-calculus mu-L is a well-known fixpoint logic to express and model check properties interpreted over labeled transition systems. In this paper, we propose two variants of the mu-calculus, mu-Lf and mu-Lf', for feature transition systems. For this, we explicitly incorporate feature expressions into the logics, allowing operators to select transitions and behavior restricted to specific…
▽ More
The modal mu-calculus mu-L is a well-known fixpoint logic to express and model check properties interpreted over labeled transition systems. In this paper, we propose two variants of the mu-calculus, mu-Lf and mu-Lf', for feature transition systems. For this, we explicitly incorporate feature expressions into the logics, allowing operators to select transitions and behavior restricted to specific products and subfamilies. We provide semantics for mu-Lf and mu-Lf' and relate the two new mu-calculi and mu-L to each other. Next, we focus on the analysis of SPL behavior and show how our formalism can be applied for product-based verification with mu-Lf as well as family-based verification with mu-Lf'. We illustrate by means of a toy example how properties can be model checked, exploiting an embedding of mu-Lf' into the mu-calculus with data.
△ Less
Submitted 1 April, 2016;
originally announced April 2016.
-
Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically
Authors:
Diego Latella,
Mieke Massink,
Erik P De Vink
Abstract:
Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process languages and their quantitative extensions in particular. In this paper, the notion of bisimulation induc…
▽ More
Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process languages and their quantitative extensions in particular. In this paper, the notion of bisimulation induced by a FuTS is addressed from a coalgebraic point of view. A correspondence result is established stating that FuTS-bisimilarity coincides with behavioural equivalence of the associated functor. As generic examples, the equivalences underlying substantial fragments of major examples of quantitative process algebras are related to the bisimilarity of specific FuTS. The examples range from a stochastic process language, PEPA, to a language for Interactive Markov Chains, IML, a (discrete) timed process language, TPC, and a language for Markov Automata, MAL. The equivalences underlying these languages are related to the bisimilarity of their specific FuTS. By the correspondence result coalgebraic justification of the equivalences of these calculi is obtained. The specific selection of languages, besides covering a large variety of process interaction models and modelling choices involving quantities, allows us to show different classes of FuTS, namely so-called simple FuTS, combined FuTS, nested FuTS, and general FuTS.
△ Less
Submitted 21 December, 2015; v1 submitted 18 November, 2015;
originally announced November 2015.
-
Rooted branching bisimulation as a congruence for probabilistic transition systems
Authors:
Matias D. Lee,
Erik P. de Vink
Abstract:
We propose a probabilistic transition system specification format, referred to as probabilistic RBB safe, for which rooted branching bisimulation is a congruence. The congruence theorem is based on the approach of Fokkink for the qualitative case. For this to work, the theory of transition system specifications in the setting of labeled transition systems needs to be extended to deal with probabil…
▽ More
We propose a probabilistic transition system specification format, referred to as probabilistic RBB safe, for which rooted branching bisimulation is a congruence. The congruence theorem is based on the approach of Fokkink for the qualitative case. For this to work, the theory of transition system specifications in the setting of labeled transition systems needs to be extended to deal with probability distributions, both syntactically and semantically. We provide a scheduler-free characterization of probabilistic branching bisimulation as adapted from work of Andova et al. for the alternating model. Counter examples are given to justify the various conditions required by the format.
△ Less
Submitted 28 September, 2015;
originally announced September 2015.
-
Coherent branching feature bisimulation
Authors:
Tessa Belder,
Maurice H. ter Beek,
Erik P. de Vink
Abstract:
Progress in the behavioral analysis of software product lines at the family level benefits from further development of the underlying semantical theory. Here, we propose a behavioral equivalence for feature transition systems (FTS) generalizing branching bisimulation for labeled transition systems (LTS). We prove that branching feature bisimulation for an FTS of a family of products coincides with…
▽ More
Progress in the behavioral analysis of software product lines at the family level benefits from further development of the underlying semantical theory. Here, we propose a behavioral equivalence for feature transition systems (FTS) generalizing branching bisimulation for labeled transition systems (LTS). We prove that branching feature bisimulation for an FTS of a family of products coincides with branching bisimulation for the LTS projection of each the individual products. For a restricted notion of coherent branching feature bisimulation we furthermore present a minimization algorithm and show its correctness. Although the minimization problem for coherent branching feature bisimulation is shown to be intractable, application of the algorithm in the setting of a small case study results in a significant speed-up of model checking of behavioral properties.
△ Less
Submitted 14 April, 2015;
originally announced April 2015.
-
Combining Insertion and Deletion in RNA-editing Preserves Regularity
Authors:
E. P. de Vink,
H. Zantema,
D. Bošnački
Abstract:
Inspired by RNA-editing as occurs in transcriptional processes in the living cell, we introduce an abstract notion of string adjustment, called guided rewriting. This formalism allows simultaneously inserting and deleting elements. We prove that guided rewriting preserves regularity: for every regular language its closure under guided rewriting is regular too. This contrasts an earlier abstractio…
▽ More
Inspired by RNA-editing as occurs in transcriptional processes in the living cell, we introduce an abstract notion of string adjustment, called guided rewriting. This formalism allows simultaneously inserting and deleting elements. We prove that guided rewriting preserves regularity: for every regular language its closure under guided rewriting is regular too. This contrasts an earlier abstraction of RNA-editing separating insertion and deletion for which it was proved that regularity is not preserved. The particular automaton construction here relies on an auxiliary notion of slice sequence which enables to sweep from left to right through a completed rewrite sequence.
△ Less
Submitted 17 November, 2012;
originally announced November 2012.
-
Bisimulation of Labeled State-to-Function Transition Systems of Stochastic Process Languages
Authors:
D. Latella,
M. Massink,
E. P. de Vink
Abstract:
Labeled state-to-function transition systems, FuTS for short, admit multiple transition schemes from states to functions of finite support over general semirings. As such they constitute a convenient modeling instrument to deal with stochastic process languages. In this paper, the notion of bisimulation induced by a FuTS is proposed and a correspondence result is proven stating that FuTS-bisimulat…
▽ More
Labeled state-to-function transition systems, FuTS for short, admit multiple transition schemes from states to functions of finite support over general semirings. As such they constitute a convenient modeling instrument to deal with stochastic process languages. In this paper, the notion of bisimulation induced by a FuTS is proposed and a correspondence result is proven stating that FuTS-bisimulation coincides with the behavioral equivalence of the associated functor. As generic examples, the concrete existing equivalences for the core of the process algebras ACP, PEPA and IMC are related to the bisimulation of specific FuTS, providing via the correspondence result coalgebraic justification of the equivalences of these calculi.
△ Less
Submitted 6 September, 2012;
originally announced September 2012.
-
Dynamic System Adaptation by Constraint Orchestration
Authors:
L. P. J. Groenewegen,
E. P. de Vink
Abstract:
For Paradigm models, evolution is just-in-time specified coordination conducted by a special reusable component McPal. Evolution can be treated consistently and on-the-fly through Paradigm's constraint orchestration, also for originally unforeseen evolution. UML-like diagrams visually supplement such migration, as is illustrated for the case of a critical section solution evolving into a pipelin…
▽ More
For Paradigm models, evolution is just-in-time specified coordination conducted by a special reusable component McPal. Evolution can be treated consistently and on-the-fly through Paradigm's constraint orchestration, also for originally unforeseen evolution. UML-like diagrams visually supplement such migration, as is illustrated for the case of a critical section solution evolving into a pipeline architecture.
△ Less
Submitted 21 November, 2008;
originally announced November 2008.
