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. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCS$η$. We also propose weak simplicial bisimilarity on polyhedral models and weak $\pm$-bisimilarity on cell poset models, 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 iff they are logically equivalent for SLCS$η$. Similarly, two cells are weakly $\pm$-bisimilar iff 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.

Segmentation of 3D medical images, and brain segmentation in particular, is an important topic in neuroimaging and in radiotherapy. Overcoming the current, time consuming, practise of manual delineation of brain tumours and providing an accurate, explainable, and replicable method of segmentation of the tumour area and related tissues is therefore an open research challenge. In this paper, we first propose a novel symbolic approach to brain segmentation and delineation of brain lesions based on spatial model checking. This method has its foundations in the theory of closure spaces, a generalisation of topological spaces, and spatial logics. At its core is a high-level declarative logic language for image analysis, ImgQL, and an efficient spatial model checker, VoxLogicA, exploiting state-of-the-art image analysis libraries in its model checking algorithm. We then illustrate how this technique can be combined with Machine Learning techniques leading to a hybrid AI approach that provides accurate and explainable segmentation results. We show the results of the application of the symbolic approach on several public datasets with 3D magnetic resonance (MR) images. Three datasets are provided by the 2017, 2019 and 2020 international MICCAI BraTS Challenges with 210, 259 and 293 MR images, respectively, and the fourth is the BrainWeb dataset with 20 (synthetic) 3D patient images of the normal brain. We then apply the hybrid AI method to the BraTS 2020 training set. Our segmentation results are shown to be in line with the state-of-the-art with respect to other recent approaches, both from the accuracy point of view as well as from the view of computational efficiency, but with the advantage of them being explainable.

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.

Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence.

Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. We explore a new domain, namely (semi-)automatic contouring in Medical Imaging, introducing the tool VoxLogicA which merges the state-of-the-art library of computational imaging algorithms ITK with the unique combination of declarative specification and optimised execution provided by spatial logic model checking. The result is a rapid , logic based analysis development methodology. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA analysis can reach state-of-the-art accuracy, competing with best-in-class algorithms, with the advantage of explainability and easy replicability . Furthermore, due to a two-orders-of-magnitude speedup compared to the existing general-purpose spatio-temporal model checker topochecker , VoxLogicA enables interactive development of analysis of 3D medical images, which can greatly facilitate the work of professionals in this domain.

In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which efficient monitoring algorithms have been developed. As such, it is suitable for real-time verification of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satisfies a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diffusion system and spatio-temporal aspects of a large bike-sharing system. Comment: 36 pages with 13 figures

Abstract Pervasive environments offer an increasing number of services to a large number of people moving within these environments, including timely information about where to go and when, and contextual information about the surrounding environment. This information may be conveyed to people through public displays or direct to a person’s mobile phone. People using these services interact with the system but they are also meeting other people and performing other activities as relevant opportunities arise. The design of such systems and the analysis of collective dynamic behaviour of people within them is a challenging problem. We present results on a novel usage of a scalable analysis technique in this context. We show the validity of an approach based on stochastic process-algebraic models by focussing on a representative example, i.e. emergency egress. The chosen case study has the advantage that detailed data is available from studies employing alternative analysis methods, making cross-methodology comparison possible. We also illustrate how realistic, context-dependent human behaviour, often observed in emergency egress, can naturally be embedded in the models, and how the effect of such behaviour on evacuation can be analysed in an efficient and scalable way. The proposed approach encompasses both the agent modelling viewpoint, as system behaviour emerges from specific (discrete) agent interaction, and the population viewpoint, when classes of homogeneous individuals are considered for a (continuous) approximation of overall system behaviour.

Pervasive environments offer an increasing number of services to a large number of people moving within these environments including timely information about where to go and when. People using these services interact with the system but they are also meeting other people and performing other activities as relevant opportunities arise. The design of such systems and the analysis of collective dynamic behaviour of people within them is a challenging problem. In previous work we have successfully explored a scalable analysis of stochastic process algebraic models of smart signage systems. In this paper we focus on the validation of a representative example of this class of models in the context of emergency egress. This context has the advantage that detailed data is available from studies with alternative analysis methods. A second aim is to show how realistic human behaviour, often observed in emergency egress, can be embedded in the model and how the effect of this behaviour on building evacuation can be analysed in an efficient and scalable way.

We report on a fruitful combination of applying academic experience with formal modelling and verification techniques to an industrial case study. The goal of the case study was to investigate a priori, i.e. before implementation, the effects of adding a lightweight and easy-to-use publish/subscribe (event) notification service to thinkteam--an asynchronous and dispersed groupware system which was developed by think3. Researchers from the Formal Methods and Tools (FM&T) group of ISTI-CNR--with a longstanding experience in research on the development and application of formal methods, notations, and software tools for the specification, design, and verification of complex computer systems--therefore teamed up with think3--a global provider of integrated product development solutions that provides mechanical design and Product Data Management (PDM) software catering the product management needs of design processes in the manufacturing industry. The technical details of this joint research effort have been documented elsewhere, here we report on the lessons learned from this experience.

Models used for the analysis of dependability and performance attributes of communication protocols often abstract considerably from the details of the actual protocol. These models often consist of concurrent sub-models and this may make it hard to judge whether their behaviour is faithfully reflecting the protocol. In this paper, we show how model checking of continuous-time Markov chains, generated from high-level specifications, facilitates the analysis of both correctness and dependability attributes. We illustrate this by revisiting a dependability analysis as stated in A. Coccoli et al. (2001)of a variant of the central access protocol of the IEEE 802.11 standard for wireless local area networks. This variant has been developed to support real-time group communication between autonomous mobile stations. Correctness and dependability properties are formally characterised using continuous stochastic logic and are automatically verified by the ETMCC model checker. The models used are specified as stochastic activity nets.

The unified modelling language has been introduced as a notation for modelling and reasoning about large and complex systems, and their design, across a wide range of application domains. System modelling and analysis techniques, especially those based on formal methods, are more and more used for enhancing traditional system engineering techniques for improving system quality. In particular this holds for model-based formal test case derivation using formal conformance testing. The contribution of the present paper is to provide a solid mathematical basis for conformance testing and automatic test case generation for UML statecharts (UMLSCs). We propose a formal conformance-testing relation for input-enabled transition systems with transitions labelled by input/output-pairs (IOLTSs). IOLTSs provide a suitable semantic model for a behavioural subset of UMLSCs. We also provide an algorithm which, for a UMLSC specification and the alphabet of implementations, generates a test suite. The algorithm is proven exhaustive and sound w.r.t. the conformance relation.

In this paper we study the formal relationship between testing preorder/equivalences for a behavioural subset of UML Statechart Diagrams and a conformance relation for implementations with respect to specifications given using such diagrams. We study the impact of stuttering on the above mentioned relationship. In the context of UMLSDs, stuttering occurs when no transition of the UMLSD is enabled by the current event in the current (global) state of the underlying state-machine. We consider both the case in which the semantics underlying the testing relations does not model stuttering explicitly - we call it the non-stuttering semantics - and the case in which it does it - i.e. the stuttering semantics. We show that in the first case the conformance relation is stronger than the reverse of the MUST preorder and, consequently, stronger than the MAY preorder. Much more interesting results can be proven in the second case, possibly under proper conditions on the sets of events under consideration. In fact the conformance relation is shown to coincide with the MAY preorder, and thus be implied by the reverse MUST preorder. Finally, we show important substitutivity properties which hold in the case of stuttering semantics.

Free flight has been proposed as a future alternative to the current policy in air traffic management (ATM) where aircraft follow predefined corridors. In free flight pilots can choose their own optimal routes, altitudes and velocities but are also responsible for the safe and fair resolution of trajectory conflicts. This would require a safe distributed control system were the trajectories that aircraft follow are as optimal as possible respecting sufficient safety distances. We model aircraft behaviour using non-determinism in such a way that reachability analysis provides the optimal trajectories of the aircraft. We compare the obtained results with the conflict resolution solutions proposed in the literature.

Haptic interfaces represent a revolution in human computer interface technology since they make it possible for users to touch and manipulate virtual objects. In this work we describe a cross‐model interaction experiment to study the effect of adding haptic cues to visual cues when vision is not enough to disambiguate the images. We relate the results to those obtained in experimental psychology as well as to more recent studies on the subject.

Much of the work concerned with virtual environments has addressed the development of new rendering technologies or interaction techniques. As the technology matures and becomes adopted in a wider range of applications, there is, however, a need to better understand how this technology can be accommodated in software engineering practice. A particular challenge presented by virtual environments is the complexity of the interaction that is supported, and sometimes necessary, for a particular task. Methods such as finite‐state automata which are used to represent and design dialogue components for more conventional interfaces, e.g. using direct manipulation within a desktop model, do not seem to capture adequately the style of interaction that is afforded by richer input devices and graphical models. In this paper, we suggest that virtual environments are, fundamentally, what are known as hybrid systems. Building on this insight, we demonstrate how techniques developed for modelling hybrid systems can be used to represent and understand virtual interaction in a way that can be used in the specification and design phases of software development, and which have the potential to support prototyping and analysis of virtual interfaces.

Abstract. Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency.

Abstract. We present the formal specification and verification of a lip-synchronisation protocol using the real-time model checker Uppaal. A number of specifications of this protocol can be found in the literature, but this is the first automatic verification. We take a published specification of the protocol, code it up in the Uppaal timed automata notation and then verify whether the protocol satisfies the key properties of jitter and skew. The verification reveals some aws in the protocol. In particular, it shows that for certain sound and video streams the protocol can time-lock before reaching a prescribed error state. We also discuss our experience with Uppaal, with particular reference to modelling timeouts and to deadlock analysis.

Abstract. The PREMO standard, Presentation Environment for Multimedia Objects, is a major new standard under development within ISO/IEC. It addresses the creation of, presentation of, and interaction with all forms of information using single or multiple media. In this paper we give a formal LOTOS specification, amenable to automatic verification, of the PREMO synchronisable object, which is one of the central parts of the standard. Various design options are investigated by a combination of constraint oriented specification and model checking. This shows the usefulness of formal specification and automatic verification during the design phase of an international standard.