pith. sign in

arxiv: 2606.31344 · v1 · pith:FCQPCN25new · submitted 2026-06-30 · 💻 cs.LO

Spatial Model Checking of Images via Minimised Models and Branching Bisimilarity

Vincenzo Ciancia , Jan Friso Groote , Diego Latella , Mieke Massink , Erik P. de Vink This is my paper

Pith reviewed 2026-07-01 03:38 UTC · model grok-4.3

classification 💻 cs.LO
keywords spatial model checkingCoPa bisimilarityquasi-discrete closure modelsbranching bisimilaritymodel minimisationlabelled transition systemsimage verification
0
0 comments X

The pith

Encoding quasi-discrete closure models as labelled transition systems lets branching bisimilarity algorithms compute CoPa equivalence classes correctly.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a minimisation procedure for spatial models represented as quasi-discrete closure models. It shows that an encoding into labelled transition systems allows standard branching bisimilarity algorithms to produce the partitions required by Compatible Paths (CoPa) bisimilarity. This preserves the forward and backward conditional reachability modalities used in spatial reasoning. The resulting method supports faster model checking of spatial properties on large models such as images while maintaining the link between equivalence classes and sets of pixels.

Core claim

For CoPa bisimilarity on quasi-discrete closure models, the encoding of closure models as labelled transition systems preserves CoPa equivalence classes, so that branching bisimilarity algorithms compute the correct partitions and thereby enable effective minimisation of spatial models.

What carries the argument

The encoding of quasi-discrete closure models as labelled transition systems, which transfers CoPa equivalence to branching bisimilarity partitions.

If this is right

  • The minimisation procedure is correct with respect to CoPa bisimilarity.
  • Model checking of spatial properties on the minimised models produces the same results as on the original models.
  • The relationship between equivalence classes and pixels in the source image is preserved by the toolchain.
  • Benchmark examples demonstrate a speed-up in checking spatial properties for models of realistic size.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same encoding strategy could be tested on closure models derived from three-dimensional voxel data.
  • Integration with existing image segmentation tools might allow automatic generation of the input closure models from raw pixel data.
  • The approach opens the possibility of applying other bisimulation-minimisation variants if they can be shown to preserve the same reachability modalities.

Load-bearing premise

The encoding of quasi-discrete closure models as labelled transition systems preserves CoPa equivalence classes.

What would settle it

A concrete quasi-discrete closure model and a spatial property such that the minimised model obtained via the encoding yields a different truth value for the property than the original model.

Figures

Figures reproduced from arXiv: 2606.31344 by Diego Latella, Erik P. de Vink, Jan Friso Groote, Mieke Massink, Vincenzo Ciancia.

Figure 1
Figure 1. Figure 1: Cross section of a dataset element of BrainWeb [ABGP+06] pat04 MRI at slice (x, y, z) = (129, 147, 78), (axial view left, coronal view middle, sagittal view right): VoxLogicA analysis of the segmentation of white matter, shown as a green overlay on top of a red overlay representing the ground truth. 1. Introduction Spatial model checking consists in the automatic verification of properties, expressed in a … view at source ↗
Figure 2
Figure 2. Figure 2: Figure 2a: A pixel based image with green and red pixels. Fig￾ure 2b: A finite, symmetric QdCM in the shape of a regular graph with nodes representing pixels and edges representing the 8-adjacency relation between the pixels of the image in Figure 2a. pixel-based, or voxel-based, image that it is given as input. Such models take the form of a symmetric regular 8-adjacency graph, in which nodes are represen… view at source ↗
Figure 3
Figure 3. Figure 3: Figure 3a: A finite QdCS (X, CR). The arrows represent the relation R underlying CR. The points of the set A ⊆ X are shown in white, remaining points are shown in black. Figure 3b: Points in CR(A)\A are shown in grey. CR satisfies all the axioms of Definition 2.3 and so (X, CR) is a CS. An example of the result of applying the closure operator CR induced by a relation R to a set A is shown in [PITH_FULL_I… view at source ↗
Figure 4
Figure 4. Figure 4: A model (a); zones in paths (b). fact, be a “minimal” — in a sense that will be made clear later in the paper — representation of the closure model. In order to relax the “counting” capability of CMC-bisimilarity for QdCSs as mentioned, a weaker notion of bisimilarity has been introduced in [CLMV22, CLMV25] that is based on paths, instead of membership of closures, together with a notion of “compatibility”… view at source ↗
Figure 5
Figure 5. Figure 5: A finite QdCM C1 {r} C2 {g} C3 {b} C4 {r} C5 {g} [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 7
Figure 7. Figure 7: (a) QdCM of [PITH_FULL_IMAGE:figures/full_fig_p014_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: A symmetric CM. As an example, consider the symmetric finite QdCM of [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: , obtained with the encoding given in Definition 4.6. The minimised model of the symmetric QdCM of [PITH_FULL_IMAGE:figures/full_fig_p018_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: The minimal symmetric CM of that in [PITH_FULL_IMAGE:figures/full_fig_p019_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: An image of a 2D maze, with green exit (upper-left), blue starting points, black walls and white walking areas (Figure 11a), its minimal LTS using the general encoding of Definition 4.1 (Figure 11b - top), and that obtained using the optimised encoding of Definition 4.6 (Figure 11b - bottom). For readability, self-loops labelled by atomic propositions are not shown; the corresponding states are shown in t… view at source ↗
Figure 12
Figure 12. Figure 12: VoxMinX toolchain for model checking via model minimisation and projection of results onto the original image. Parts 3 and 9 in blue are command line operations of the mCRL2 toolset. Parts 2, 4, 7 and 11 in purple are developed in Python in the context of the current paper. The orange parts 5, 8 and 10 are intermediate data structures. Parts 1 and 6 in yellow are the input and part 12 in red is the output… view at source ↗
Figure 13
Figure 13. Figure 13: Maze example (4096x4096). Figure 13a original image. Fig￾ure 13b is showing the model checking results in which pixels satisfying ϕ maze 1 are shown in white, others are shown in black. Figure 13c shows an alternative visualisation of the same results where pixels satisfying formula ϕ maze 1 are highlighted (white), others are grey-shaded. The green exit is situated in the top left corner of the maze in F… view at source ↗
Figure 14
Figure 14. Figure 14: Pacman example (200x200 pixels). Figure 14a original image. Figure 14b shows pixels satisfying formula ghosts in white, others are shown in black. Figure 14c pixels satisfying formula ghosts as highlighted colours, others are shown in shaded colours. Next, let us have a closer look at the other parts of the toolchain in [PITH_FULL_IMAGE:figures/full_fig_p024_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Minimal LTS of the Pac-Man image shown in Figure 14a. State colours correspond to colours in the image and states are numbered for convenience of reference. Each state corresponds to an equivalence class. There are 35 classes. The class in the centre (state 4) is black and corresponds to the background of the image. The label denoting ‘change’ at all transitions, as well as all self-loops and related labe… view at source ↗
Figure 16
Figure 16. Figure 16: Monoscope test pattern Philips PM5544 names of the images in each family are composed of their name (maze, mono, pm) followed by a numeric indication of the vertical resolution of each image. The maze and the Pac-Man images are square, therefore their horizontal resolution coincides with their vertical one. For example, maze-1024 is a png image of the maze of 1024 pixels wide and 1024 pixels high. The mon… view at source ↗
Figure 17
Figure 17. Figure 17: VoxMinX: Model size in number of states vs. speed-up factor for the maze (blue), the monoscope (red) and the Pac-Man (brown) examples (17a). For the same models: number of states vs. model checking of full model with VoxLogicA (17b) and number of states vs. minimisation time without IO (17c). by the ICRL logic. (In-)finitary Compatible Reachability Logic includes conjunction and two conditional reachabili… view at source ↗
Figure 18
Figure 18. Figure 18: Running example: 4 pixels, 1 blue and 3 white Appendix A. Running Example for VoxMinX To illustrate the various intermediate steps of the VoxMin toolchain in [PITH_FULL_IMAGE:figures/full_fig_p039_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Running example model checking result for atomic proposition white: 4 pixels, 1 black and 3 white. This result can be projected (see Box 11 in [PITH_FULL_IMAGE:figures/full_fig_p043_19.png] view at source ↗
read the original abstract

Spatial models are of increasing interest in traditional computer science domains and beyond. Spatial minimisation procedures are crucial for efficient model checking of such models that are often large in size. For the recent notion of spatial bisimilarity for quasi-discrete closure models, called `Compatible Paths' (CoPa) bisimilarity, an effective minimisation method is proposed, and shown to be correct. Reasoning about space represented by quasi-discrete closure models involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality, representing the fact that a point can be reached from another point, under certain conditions. The core of our minimisation method is the encoding of closure models as labelled transition systems, enabling minimisation algorithms for branching bisimilarity to compute CoPa equivalence classes. A prototype toolchain, VoxMinX, is proposed to validate the minimisation method. VoxMinX preserves the relationship between equivalence classes and sets of pixels in the original image. Experimental validation of the toolchain via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper proposes a minimisation procedure for Compatible Paths (CoPa) bisimilarity on quasi-discrete closure models by encoding them as labelled transition systems (LTS), so that standard branching bisimilarity algorithms compute the CoPa partitions. It presents the VoxMinX toolchain that preserves the correspondence between equivalence classes and pixel sets in images, and reports experimental speed-ups on benchmark spatial model-checking tasks.

Significance. If the encoding is shown to preserve CoPa equivalence classes bidirectionally, the method would allow reuse of mature branching-bisimilarity tools for spatial verification, yielding practical speed-ups on realistically sized image models while maintaining the link to the original pixel sets. The experimental component and the toolchain constitute concrete strengths.

major comments (1)
  1. [Encoding and correctness argument (core of the minimisation method)] The bidirectional preservation claim (points p,q are CoPa-bisimilar iff their LTS images are branching-bisimilar) is load-bearing for the entire minimisation method. The abstract states that the encoding is shown correct, yet the manuscript must supply an explicit argument that both the forward and backward conditional reachability modalities, together with the compatibility condition on paths, are faithfully represented by the LTS transition relation and labels; any gap here would mean the computed partitions are not exactly the CoPa classes.
minor comments (2)
  1. [Toolchain description] The relationship between the original pixel sets and the equivalence classes after minimisation should be stated more explicitly in the description of VoxMinX.
  2. [Experimental validation] Benchmark tables would benefit from reporting both the size of the original model and the size of the minimised model alongside the observed speed-up factors.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the thorough review and for identifying the need for greater explicitness in the correctness argument. We address the major comment below.

read point-by-point responses

  1. Referee: The bidirectional preservation claim (points p,q are CoPa-bisimilar iff their LTS images are branching-bisimilar) is load-bearing for the entire minimisation method. The abstract states that the encoding is shown correct, yet the manuscript must supply an explicit argument that both the forward and backward conditional reachability modalities, together with the compatibility condition on paths, are faithfully represented by the LTS transition relation and labels; any gap here would mean the computed partitions are not exactly the CoPa classes.

    Authors: We agree that an explicit, self-contained argument for bidirectional preservation is essential. The current manuscript states correctness but does not spell out the details for the backward modality and the path-compatibility condition in a single place. In the revision we will add a dedicated subsection (new Section 4.3) that (i) recalls the definitions of the two conditional reachability modalities and the compatibility predicate, (ii) shows how each is encoded by the LTS transition relation and labels, and (iii) proves both directions of the equivalence (CoPa bisimilarity iff branching bisimilarity on the image LTS). This will make the load-bearing claim fully rigorous. revision: yes

Circularity Check

0 steps flagged

No circularity: correctness via explicit bidirectional preservation proof for the LTS encoding

full rationale

The core claim is that an encoding of quasi-discrete closure models into LTSs preserves CoPa equivalence classes in both directions, allowing standard branching-bisimilarity minimisation algorithms to compute the correct partitions. This is a standard reduction whose soundness rests on a preservation argument relating the closure operator and compatible-paths condition to the transition relation and labels; the argument is not shown to reduce to a self-citation, a fitted parameter, or a definitional identity. No self-definitional, fitted-input, or uniqueness-imported-from-authors patterns appear. The method is therefore self-contained against external branching-bisimilarity algorithms.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on standard definitions of closure models, CoPa bisimilarity, and branching bisimilarity; no free parameters or new entities are introduced in the abstract.

axioms (2)
  • domain assumption Quasi-discrete closure models and CoPa bisimilarity are well-defined and the relevant notions from prior work
    The paper builds directly on these recent spatial bisimilarity concepts without re-deriving them.
  • standard math Branching bisimilarity minimisation algorithms for LTS are correct and available
    The method delegates equivalence class computation to these established algorithms.

pith-pipeline@v0.9.1-grok · 5740 in / 1237 out tokens · 52124 ms · 2026-07-01T03:38:31.255754+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

300 extracted references · 13 canonical work pages

  1. [1]

    Jansen , editor =

    Jan Friso Groote and David N. Jansen , editor =. A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity , booktitle =. 2025 , url =

    2025

  2. [2]

    Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference,

    Martens, Jan and Laveaux, Maurice , title =. Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference,. 2026 , url =. doi:10.1007/978-3-032-22752-2 , isbn =

    work page doi:10.1007/978-3-032-22752-2 2026

  3. [3]

    Practical Polyhedral Model Checking

    Andriaccio, Yuri and Ciancia, Vincenzo and Latella, Diego and Massink, Mieke. Practical Polyhedral Model Checking. Journeys Between Formal Methods and the Railway Industry: Essays Dedicated to Alessandro Fantechi on the Occasion of His 70th Birthday. 2026. doi:10.1007/978-3-032-12484-5_8

    work page doi:10.1007/978-3-032-12484-5_8 2026

  4. [4]

    Model Checking in Space with Applications to Medical Image Analysis - Invited Abstract , booktitle =

    Gina Belmonte and Vincenzo Ciancia and Diego Latella and Mieke Massink , editor =. Model Checking in Space with Applications to Medical Image Analysis - Invited Abstract , booktitle =. 2026 , url =

    2026

  5. [5]

    Ten Years of Spatial Model Checking , booktitle =

    Vincenzo Ciancia and Diego Latella and Mieke Massink , editor =. Ten Years of Spatial Model Checking , booktitle =. 2025 , url =

    2025

  6. [6]

    2504.13846 , archivePrefix=

    Antonio Strippoli , year=. 2504.13846 , archivePrefix=

    work page arXiv

  7. [7]

    de Vink , title =

    Nick Bezhanishvili and Laura Bussi and Vincenzo Ciancia and David Gabelaia and Mamuka Jibladze and Diego Latella and Mieke Massink and Erik P. de Vink , title =. Log. Methods Comput. Sci. , volume =. 2026 , url =

    2026

  8. [8]

    and Weijland, W.P

    Baeten, J.C.M. and Weijland, W.P. , title=. 1990 , collection=

    1990

  9. [9]

    2014 , url =

    Jan Friso Groote and Mohammad Reza Mousavi , title =. 2014 , url =

    2014

  10. [10]

    and Liu, Xiaoxiao and Ibanez, Luis and Jomier, Julien and Marion, Charles , TITLE=

    McCormick, Matthew M. and Liu, Xiaoxiao and Ibanez, Luis and Jomier, Julien and Marion, Charles , TITLE=. Frontiers in Neuroinformatics , VOLUME=. 2014 , URL=

    2014

  11. [11]

    Lowekamp and David T

    Bradley C. Lowekamp and David T. Chen and Luis Ib. The Design of SimpleITK , journal =. 2013 , url =. doi:10.3389/FNINF.2013.00045 , timestamp =

    work page doi:10.3389/fninf.2013.00045 2013

  12. [12]

    Michele Loreti and Michela Quadrini , title =. Log. Methods Comput. Sci. , volume =. 2023 , url =. doi:10.46298/LMCS-19(3:8)2023 , timestamp =

    work page doi:10.46298/lmcs-19(3:8)2023 2023

  13. [13]

    de , editor =

    Vincenzo Ciancia and David Gabelaia and Diego Latella and Mieke Massink and Vink, Erik P. de , editor =. On Bisimilarity for Polyhedral Models and. Formal Techniques for Distributed Objects, Components, and Systems - 43rd. 2023 , url =. doi:10.1007/978-3-031-35355-0\_9 , timestamp =

    work page doi:10.1007/978-3-031-35355-0 2023

  14. [14]

    de , editor =

    Nick Bezhanishvili and Vincenzo Ciancia and David Gabelaia and Mamuka Jibladze and Diego Latella and Mieke Massink and Vink, Erik P. de , editor =. Weak Simplicial Bisimilarity for Polyhedral Models and. Formal Techniques for Distributed Objects, Components, and Systems - 44th. 2024 , url =. doi:10.1007/978-3-031-62645-6\_2 , timestamp =

    work page doi:10.1007/978-3-031-62645-6 2024

  15. [15]

    2025 , month =

    On Bisimilarity for Quasi-discrete Closure Spaces , author =. 2025 , month =. doi:10.46298/lmcs-21(3:21)2025 , journal =

    work page doi:10.46298/lmcs-21(3:21)2025 2025

  16. [16]

    Jaeger and Simon A

    Fabian Isensee and Paul F. Jaeger and Simon A. A. Kohl and Jens Petersen and Klaus H. Maier-Hein , title =. Nature Methods , publisher =. 2021 , url =

    2021

  17. [17]

    Fabian Isensee and Tassilo Wald and Constantin Ulrich and Michael Baumgartner and Saikat Roy and Klaus H. Maier. Medical Image Computing and Computer Assisted Intervention -. 2024 , url =

    2024

  18. [18]

    Gina Belmonte and Vincenzo Ciancia and Mieke Massink , title =. Artif. Intell. Medicine , publisher =. 2025 , url =

    2025

  19. [19]

    de , editor =

    Vincenzo Ciancia and Jan Friso Groote and Diego Latella and Mieke Massink and Vink, Erik P. de , editor =. Minimisation of Spatial Models Using Branching Bisimilarity , booktitle =. 2023 , url =

    2023

  20. [20]

    , title =

    Ciancia, Vincenzo and Groote, Jan Friso and Latella, Diego and Massink, Mieke and de Vink, Erik P. , title =. doi:10.5281/zenodo.7393236 , url =

    work page doi:10.5281/zenodo.7393236

  21. [21]

    2022 , doi =

    Vincenzo Ciancia and Jan Friso Groote and Diego Latella and Mieke Massink and Erik P. 2022 , doi =

    2022

  22. [22]

    2009 , isbn =

    Robin Milner , title =. 2009 , isbn =

    2009

  23. [23]

    Ariadne: Topology Aware Adaptive Security for Cyber-Physical Systems , booktitle =

    Christos Tsigkanos and Liliana Pasquale and Carlo Ghezzi and Bashar Nuseibeh , editor =. Ariadne: Topology Aware Adaptive Security for Cyber-Physical Systems , booktitle =. 2015 , url =

    2015

  24. [24]

    Gordon , editor =

    Luca Cardelli and Andrew D. Gordon , editor =. Anytime, Anywhere: Modal Logics for Mobile Ambients , booktitle =. 2000 , url =

    2000

  25. [25]

    A spatial logic for concurrency (part

    Lu. A spatial logic for concurrency (part. Inf. Comput. , volume =. 2003 , url =

    2003

  26. [26]

    Cohn and Jochen Renz , editor =

    Anthony G. Cohn and Jochen Renz , editor =. Qualitative Spatial Representation and Reasoning , booktitle =. 2008 , url =

    2008

  27. [27]

    , School =

    Aiello, M. , School =. Spatial Reasoning: Theory and Practice , Year =

  28. [28]

    , journal =

    Aiello, M. , journal =. The topo-approach to spatial representation and reasoning , volume =

  29. [29]

    Spatial Model Checking with mCRL2

    Floris Zeven. Spatial Model Checking with mCRL2. 2022

    2022

  30. [30]

    van and W

    Glabbeek, Rob J. van and W. P. Weijland , title =. J. 1996 , url =

    1996

  31. [31]

    Jansen and Jan Friso Groote and Jeroen J.A

    David N. Jansen and Jan Friso Groote and Jeroen J.A. Keiren and Anton Wijs , editor =. An. Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference,. 2020 , url =

    2020

  32. [32]

    Olav Bunte and Jan Friso Groote and Jeroen J. A. Keiren and Maurice Laveaux and Thomas Neele and Erik P. de Vink and Wieger Wesselink and Anton Wijs and Tim A. C. Willemse , editor =. The. Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference,. 2019 , url =

    2019

  33. [33]

    Smyth and Julian Webster , editor =

    Michael B. Smyth and Julian Webster , editor =. Discrete Spatial Models , booktitle =. 2007 , url =

    2007

  34. [34]

    2007 , url =

    Handbook of Modal Logic , series =. 2007 , url =

    2007

  35. [35]

    and Griffin, M

    Aubert-Broche, B. and Griffin, M. and Pike, G.B. and Evans, A.C. and Collins, D.L. , journal=. Twenty New Digital Brain Phantoms for Creation of Validation Image Data Bases , year=

  36. [36]

    Marchetti and Noel C.F

    Michael A. Marchetti and Noel C.F. Codella and Stephen W. Dusza and David A. Gutman and Brian Helba and Aadi Kalloo and Nabin Mishra and Cristina Carrera and M. Emre Celebi and Jennifer L. DeFazio and Natalia Jaimes and Ashfaq A. Marghoob and Elizabeth Quigley and Alon Scope and Oriol Y\'. Results of the 2016 International Skin Imaging Collaboration Inter...

    2016

  37. [37]

    SpaTeL: a novel spatial-temporal logic and its applications to networked systems , booktitle =

    Iman Haghighi and Austin Jones and Zhaodan Kong and Ezio Bartocci and Radu Grosu and Calin Belta , editor =. SpaTeL: a novel spatial-temporal logic and its applications to networked systems , booktitle =. 2015 , url =

    2015

  38. [38]

    Feasibility of Spatial Model Checking for Nevus Segmentation , booktitle =

    Gina Belmonte and Giovanna Broccia and Vincenzo Ciancia and Diego Latella and Mieke Massink , editor =. Feasibility of Spatial Model Checking for Nevus Segmentation , booktitle =. 2021 , url =

    2021

  39. [39]

    Smolka and Flavio Corradini and Anita Wasilewska and Emilia Entcheva and Ezio Bartocci , title =

    Radu Grosu and Scott A. Smolka and Flavio Corradini and Anita Wasilewska and Emilia Entcheva and Ezio Bartocci , title =. Commun. 2009 , url =

    2009

  40. [40]

    CoRR , volume =

    Michele Loreti and Michela Quadrini , title =. CoRR , volume =. 2021 , url =. 2105.08708 , timestamp =

    work page arXiv 2021

  41. [41]

    2022 , month = Nov, keywords =

    Nick Bezhanishvili and Vincenzo Ciancia and David Gabelaia and Gianluca Grilletti and Diego Latella and Mieke Massink , url =. 2022 , month = Nov, keywords =. doi:10.46298/lmcs-18(4:7)2022 , journal =

    work page doi:10.46298/lmcs-18(4:7)2022 2022

  42. [42]

    Colin Stirling , title =

  43. [43]

    Natasha Kurtonina and Maarten de Rijke , title =. J. Log. Lang. Inf. , volume =. 1997 , url =

    1997

  44. [44]

    Logical Methods in Computer Science , volume =

    Laura Nenzi and Luca Bortolussi and Vincenzo Ciancia and Michele Loreti and Mieke Massink , title =. Logical Methods in Computer Science , volume =. 2018 , url =

    2018

  45. [45]

    A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems , booktitle =

    Vincenzo Ciancia and Diego Latella and Mieke Massink and Rytis Paskauskas and Andrea Vandin , editor =. A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems , booktitle =. 2016 , url =

    2016

  46. [46]

    Analysing Spatial Properties on Neighbourhood Spaces , booktitle =

    Sven Linker and Fabio Papacchini and Michele Sevegnani , editor =. Analysing Spatial Properties on Neighbourhood Spaces , booktitle =. 2020 , url =

    2020

  47. [47]

    An Experimental Spatio-Temporal Model Checker , booktitle =

    Vincenzo Ciancia and Gianluca Grilletti and Diego Latella and Michele Loreti and Mieke Massink , editor =. An Experimental Spatio-Temporal Model Checker , booktitle =. 2015 , url =

    2015

  48. [48]

    Vaandrager , editor =

    Jan Friso Groote and Frits W. Vaandrager , editor =. An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence , booktitle =. 1990 , url =

    1990

  49. [49]

    Embedding

    Vincenzo Ciancia and Diego Latella and Mieke Massink , editor =. Embedding. Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday , series =. 2019 , url =

    2019

  50. [50]

    Randell and Gabriel Landini and Antony Galton , title =

    David A. Randell and Gabriel Landini and Antony Galton , title =. 2013 , url =

    2013

  51. [51]

    Vincenzo Ciancia and Stephen Gilmore and Gianluca Grilletti and Diego Latella and Michele Loreti and Mieke Massink , title =. Int. J. Softw. Tools Technol. Transf. , volume =. 2018 , url =

    2018

  52. [52]

    Specifying and Verifying Properties of Space , booktitle =

    Vincenzo Ciancia and Diego Latella and Michele Loreti and Mieke Massink , editor =. Specifying and Verifying Properties of Space , booktitle =. 2014 , url =

    2014

  53. [53]

    de , editor =

    Vincenzo Ciancia and Diego Latella and Mieke Massink and Vink, Erik P. de , editor =. A Journey From Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday , series =. doi:10.1007/978-3-031-15629-8\_6 , year =

    work page doi:10.1007/978-3-031-15629-8

  54. [54]

    Vincenzo Ciancia and Diego Latella and Mieke Massink and Vink, Erik de , year=

  55. [55]

    de , title =

    Vincenzo Ciancia and Diego Latella and Mieke Massink and Vink, Erik P. de , title =. CoRR , volume =. 2021 , url =. 2105.06690 , timestamp =

    work page arXiv 2021

  56. [56]

    Jansen and Jeroen J

    Jan Friso Groote and David N. Jansen and Jeroen J. A. Keiren and Anton Wijs , title =. 2017 , url =

    2017

  57. [57]

    VoxLogicA:

    Gina Belmonte and Vincenzo Ciancia and Diego Latella and Mieke Massink , editor =. VoxLogicA:. Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference,. 2019 , url =

    2019

  58. [58]

    Innovating Medical Image Analysis via Spatial Logics , booktitle =

    Gina Belmonte and Vincenzo Ciancia and Diego Latella and Mieke Massink , editor =. Innovating Medical Image Analysis via Spatial Logics , booktitle =. 2019 , url =

    2019

  59. [59]

    Spatial logics and model checking for medical imaging , journal =

    Fabrizio. Spatial logics and model checking for medical imaging , journal =. 2020 , url =

    2020

  60. [60]

    Browne and Edmund M

    Michael C. Browne and Edmund M. Clarke and Orna Grumberg , title =. Theor. Comput. Sci. , volume =. 1988 , url =

    1988

  61. [61]

    2020 , eprint=

    Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations , author=. 2020 , eprint=

    2020

  62. [62]

    Logical Methods in Computer Science , volume =

    Vincenzo Ciancia and Diego Latella and Michele Loreti and Mieke Massink , title =. Logical Methods in Computer Science , volume =. 2016 , url =

    2016

  63. [63]

    A generalized topological view of motion in discrete space

    Galton, A. A generalized topological view of motion in discrete space. 2003

    2003

  64. [64]

    Modal Logics of Space , booktitle =

    Benthem, Johan van and Guram Bezhanishvili , editor =. Modal Logics of Space , booktitle =. 2007 , url =

    2007

  65. [65]

    Benthem, Johan van and Nick Bezhanishvili and Sebastian Enqvist and Junhua Yu , title =. Rev. Symb. Log. , volume =. 2017 , url =

    2017

  66. [66]

    2020 , NOTE =

    Morris,. 2020 , NOTE =

    2020

  67. [67]

    2003 , NOTE =

    Hansen,. 2003 , NOTE =

    2003

  68. [68]

    2009 , MONTH = Apr, KEYWORDS =

    Hansen,. 2009 , MONTH = Apr, KEYWORDS =

    2009

  69. [69]

    Universal coalgebra: a theory of systems

    Rutten, J. Universal coalgebra: a theory of systems. 2000

    2000

  70. [70]

    and Massink, M

    Latella, D. and Massink, M. and Vink, E.P. de. Bisimulation of Labeled State-to-Function Transition Systems Coalgebraically. 2015

    2015

  71. [71]

    Ad\'amek and H.-E

    J. Ad\'amek and H.-E. Porst , title =. Theoretical Computer Science , year = 2004, volume = 311, pages =

    2004

  72. [72]

    Ad\'amek and S

    J. Ad\'amek and S. Milius and L.S. Moss , title =

  73. [73]

    Back and Forth Bisimulations , booktitle =

    Rocco. Back and Forth Bisimulations , booktitle =. 1990 , url =

    1990

  74. [74]

    van , editor =

    Glabbeek, Rob J. van , editor =. The Linear Time-Branching Time Spectrum (Extended Abstract) , booktitle =. 1990 , url =

    1990

  75. [75]

    1989 , isbn =

    Robin Milner , title =. 1989 , isbn =

    1989

  76. [76]

    Rieser , title =

    A. Rieser , title =. Topology and its Applications , year = 2021, volume = 296, pages = 107613, url =

    2021

  77. [77]

    Ciancia, Vincenzo and Mieke Massink , title =

  78. [78]

    Bradfield and Colin Stirling , editor =

    Julian C. Bradfield and Colin Stirling , editor =. Modal mu-calculi , booktitle =. 2007 , url =

    2007

  79. [79]

    Theories and Experiences for Real-Time System Development

    Theories and Experiences for Real-Time System Development. Theories and Experiences for Real-Time System Development

  80. [80]

    Handbook of Process Algebra

    Handbook of Process Algebra. Handbook of Process Algebra

Showing first 80 references.