Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operational perspectives is important, for both foundations and applications. This paper takes an important step towards such a correspondence, by precisely relating bi-Kleene Algebra (BKA), a fragment of CKA, to a novel type of automata, pomset automata (PAs). We show that PAs can implement the BKA semantics of series-parallel rational expressions, and that a class of PAs can be translated back to these expressions. We also characterise the behavior of general PAs in terms of context-free pomset grammars; consequently, universality, equivalence and series-parallel rationality of general PAs are undecidable.
The classical subset construction for non-deterministic automata can be generalized to other side-effects captured by a monad. The key insight is that both the state space of the determinized automaton and its semantics—languages over an alphabet—have a common algebraic structure: they are Eilenberg-Moore algebras for the powersetgen monad. In this paper we study the reverse question to determinization. We will present a construction to associate succinct automata to languages based on different algebraic structures. For instance, for classical regular languages the construction will transform a deterministic automaton into a non-deterministic one, where the states represent the join-irreducibles of the language accepted by a (potentially) larger deterministic automaton. Other examples will yield alternating automata, automata with symmetries, CABA-structured automata, and weighted automata.
Partial order and structural reduction techniques are some of the most beneficial methods for state space reduction in reachability analysis of Petri nets. This is among others documented by the fact that these techniques are used by the leading tools in the annual Model Checking Contest (MCC) of Petri net tools. We suggest improved versions of a partial order reduction based on stubborn sets and of a structural reduction with additional new reduction rules, and we extend both methods for the application on Petri nets with weighted arcs and weighted inhibitor arcs. All algorithms are implemented in the open source verification tool TAPAAL and evaluated on a large benchmark of Petri net models from MCC'17, including a comparison with the tool LoLA (the last year winner of the competition). The experiments document that both methods provide significant state space reductions and, even more importantly, that their combination is indeed beneficial as a further nontrivial state space reduction can be achieved. (C) 2018 Elsevier Inc. All rights reserved.
Time Geography is a framework for describing reachable points in a (static) spatio-temporal environment. While originally devised to facilitate reasoning about an individual's or a population's living conditions, it was later adapted to many other applications. A wayfinder is an entity that moves through a space-time continuum with possible obstacles. We show how to model the pertinent notions in relational algebra (and, more abstractly, in modal semirings) with box and diamond operators. Admissible or undesired regions can be described as Boolean combinations of primitive regions such as the set of all points reachable by forward or backward movement from a given region or starting point. To derive results about the region blocked by the union of two regions we introduce an abstract algebraic view of coordinates that is largely independent of dimensional and metric aspects and thus very general. Moreover, the approach lends itself quite well to machine-supported proofs.
For models of concurrent and distributed systems, it is important and also challenging to establish correctness in terms of safety and/or liveness properties. Theories of distributed systems consider equivalences fundamental, since they (1) preserve desirable correctness characteristics and (2) often allow for component substitution making compositional reasoning feasible. Modeling distributed systems often requires abstraction utilizing nondeterminism which induces unintended behaviors in terms of infinite executions with one nondeterministic choice being recurrently resolved, each time neglecting a single alternative. These situations are considered unrealistic or highly improbable. Fairness assumptions are commonly used to filter system behaviors, thereby distinguishing between realistic and unrealistic executions. This allows for key arguments in correctness proofs of distributed systems, which would not be possible otherwise. Our contribution is an equivalence spectrum in which fairness assumptions are preserved. The identified equivalences allow for (compositional) reasoning about correctness incorporating fairness assumptions.
Input-output conformance simulation (iocos_ ) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretmans' classic ioco relation, but has better worst-case complexity than ioco and supports stepwise refinement. The goal of this paper is to develop the theory of iocos_ by studying logical characterisations of this relation, rule formats for it and its compositionality. More specifically, this article presents characterisations of iocos_ in terms of modal logics and compares them with an existing logical characterisation for ioco proposed by Beohar and Mousavi. It also offers a characteristic-formula construction for iocos_ over finite processes in an extension of the proposed modal logics with greatest fixed points. A precongruence rule format for iocos_ and a rule format ensuring that operations take quiescence properly into account are also given. Both rule formats are based on the GSOS format by Bloom, Istrail and Meyer. The general modal decomposition methodology of Fokkink and van Glabbeek is used to show how to check the satisfaction of properties expressed in the logic for iocos_ in a compositional way for operations specified by rules in the precongruence rule format for iocos_ .
In the setting of the π-calculus with binary sessions, we aim at relaxing the notion of duality of session types by the concept of retractable compliance developed in contract theory. This leads to extending session types with a new type operator of “speculative selection” including choices not necessarily offered by a compliant partner. We address the problem of selecting successful communicating branches by means of an operational semantics based on orchestrators, which has been shown to be equivalent to the retractable semantics of contracts, but clearly more feasible. A type system, sound with respect to such a semantics, is hence provided. The introduction of subtyping when interactions are orchestrated naturally leads to explicit subtyping, where coercions are functors on orchestrators. Besides, priority-governed selection policies (either at type- or process-level) are investigated in order to get rid of nondeterministic behaviours but those of the partner processes of the interactions.
In this paper we present an approach to pointless topology that is based on the study of the membership or is-element-of relation within a typed or categorical version of the component-free calculus of relations. This allows us to study several other approaches to topology, including point-set topology, on an abstract and component-free level. In particular, we will show that topologies defined by open sets, closed sets, a family of neighbourhood systems, a topological kernel-mapping, a Kuratowski closure-mapping, or a topological Aumann contact relation are cryptomorphic concepts, i.e., each concept can bijectively be transformed into any other of these concepts. All transformations are specified via relation-algebraic expressions which, in case of set-theoretic relations (that is, in case of point-set topology) can immediately be executed by the specific purpose computer algebra system RelView.
In concurrency theory, weak bisimilarity is often used to relate processes exhibiting the same observable behaviour. The probabilistic environment gives rise to several generalisations; we study the infinitary semantics, which abstracts from a potentially unbounded number of internal actions being performed when something observable happens. Arguing that this notion yields the most desirable properties, we provide a sound and complete axiomatisation capturing its essence. Previous research has failed to achieve completeness in the presence of unguarded recursion, as only the finitary variant has been axiomatised, yet.
A multitude of weak memory models exists supporting various types of relaxations and different synchronization primitives. On one hand, such models must be lax enough to account for hardware and compiler optimizations; on the other, the more lax the model, the harder it is to understand and program for. Though the right balance is up for debate, a memory model should provide what is known as the SC-DRF guarantee, meaning that data-race free programs behave in a sequentially consistent manner. We present a weak memory model for a calculus inspired by the Go programming language. Thus, different from previous approaches, we focus on a memory model with buffered channel communication as the sole synchronization primitive. We formalize our model via an operational semantics, which allows us to prove the SC-DRF guarantee using a standard simulation technique. Contrasting against an axiomatic semantics, where the notion of a program is abstracted away as a graph with memory events as nodes, we believe our semantics and simulation proof can be clearer and easier to understand. Finally, we provide a concrete implementation in 𝕂 , a rewrite-based executable semantic framework, and derive an interpreter for the proposed language.
Security risk assessment and prevention in ICT systems rely on the analysis of data on the joint behavior of the system and its (malicious) users. The Haruspex tool models intelligent, goal-oriented agents that reach their goals through attack sequences. Data is synthetically generated through a Monte Carlo method that runs multiple simulations of the attacks against the system. In this paper, we present a sequential pattern mining analysis of the database of attack sequences. The intended objective is twofold: (1) to exploit the extracted patterns for the design of attack counter-measures, and (2) for gaining a better understanding of the "degree of freedom" available for the attackers of a system. We formally motivate the need for using maximal sequential patterns, instead of frequent or closed sequential patterns, and report on the results on a specific case study.
We give the first non-interleaving early operational semantics for the pi-calculus which generalizes the standard interleaving semantics and unfolds to the stable model of prime event structures. Our starting point is the non-interleaving semantics given for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject) causality and events are defined from a notion of locations derived from the syntactic structure of the process terms. The semantics is conservatively extended with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the dynamic communication topology of the pi-calculus. We prove that the semantics generalises both the standard interleaving early semantics for the pi-calculus and the non-interleaving semantics for CCS. In particular, it gives rise to a labelled asynchronous transition system unfolding to prime event structures.
Petri nets can express concurrency and nondeterminism but neither locality nor hierarchy. This article presents an extension of Petri nets, in which places can be grouped into so-called “units” expressing sequential components. Units can be recursively nested to reflect both the concurrent and hierarchical nature of complex systems. This model called NUPN (Nested-Unit Petri Nets) was originally developed for translating process calculi to Petri nets, but later found also useful beyond this setting. It allows significant savings in the memory representation of markings for both explicit-state and symbolic verification. Thirteen software tools already implement the NUPN model, which has also been adopted for the benchmarks of the Model Checking Contest (MCC) and the parallel problems of the Rigorous Examination of Reactive Systems (RERS) challenges.
We propose a new algebraic approach to graph transformation, called the Pullback-Pushout ( pbpo ) approach, where we combine smoothly the classical modifications to a host graph specified by a first part of a rule, defined as a span of graph morphisms, with the cloning of structures specified by a second span. The motivation behind this new approach is to support cloning of structures in an elegant and efficient way. After a formal definition of the proposed approach, we demonstrate that pbpo rewriting is a conservative extension of agree and the Sesqui-Pushout approaches. Contrary to agree , we show that the proposed pbpo transformation can easily be extended to cope with attributed graphs. In general, totally attributed graphs are not closed under pbpo transformation. We propose sufficient conditions which guarantee that the attribution of transformed graphs is total. Furthermore, a pbpo transformation can affect all parts of a host graph including non local parts (i.e., parts which are outside the image of the left-hand side of a rule). We propose and discuss some conditions which ensure a form of locality of pbpo transformations.
Linearisability is a central notion for verifying concurrent libraries: a library is proven correct if its operational history can be rearranged into a sequential one that satisfies a given specification. Until now, linearisability has been examined for libraries in which method arguments and method results were of ground type. In this paper we extend linearisability to the general higher-order setting, where methods of arbitrary type can be passed as arguments and returned as values, and establish its soundness.
The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.
For a subset system Z and a subset selection Γ of Z−sets, we introduce two special types of subsets of a poset, called ΔΓ−continuously ⋁−existing subsets and ΔΓ−closed subsets. We define the ZΓ−completion ZΓ(P) to be the set of all ΔΓ−continuously ⋁−existing, ΔΓ−closed subsets of a given poset P. We prove that if Z is subset-hereditary, then (1) the ZΓ−completion ZΓ(P) is the smallest Z−complete subposet containing all principal ideals in the set of all ΔΓ−closed subsets of P; (2) any ΔΓ−continuous function f:P→L mapping into a Z−complete poset L extends uniquely to a Z∨−continuous function from the completion ZΓ(P) to L. The ZΓ−completion includes numerous special cases: the Dedekind-MacNeille completion, the Frink ideal completion, the ideal completion, the Z−completion, the Hoare powerdomain, etc.
Actor Networks are a modelling framework for cyber-physical-system protocols based on Latour's actor-network theory that addresses the way we now create and exploit the power of networks whose components are no longer limited to programs, but can also include humans and physical artefacts as actors. The main contribution of this paper is a logic for modelling and reasoning about such actor networks that results from a two-stage constrained-hybridisation process: the first stage corresponds to a logic that captures the structure of actor networks and the way knowledge or data flows across them; the second addresses their dynamic aspects, i.e., the way actor networks can evolve as a result of the interactions that occur within them. For each of these stages, we develop a sound and complete proof system, and we illustrate how the framework can be used for modelling and analysing properties of cyber-physical-system protocols. This two-stage constrained-hybridisation process advances the theoretical and practical aspects of hybrid logics by providing new insights and results that go beyond the specific domain of actor networks. On the other hand, and in line with Milner's bigraph paradigm, the paper also makes a novel contribution to the development of formal methods for systems where connectivity and locality play a fundamental role.
Functional variation is an important fundamental mathematical theory widely used in engineering analysis, especially in dynamics based design. However, its formalization still remains unexplored and this makes the verification of dynamic properties of engineering structures quite cumbersome. The present paper aims at initiating the formalization of this theory. For this purpose, the function-space theory is first formalized and then it is formally proved that this continuous function space is a Banach space. Then, linear functionals based on this function space are formalized. Further, the functional variation in the Fréchet derivative form and its main properties are formalized. Then the necessary condition of functional extrema is formally verified. Lastly, we formally verify the continuous functional and mean value theorem of functional variation for demonstrating the application of the formalized functional variation. The present formalization work can serve as a foundation for the formal verification of dynamic behavior of mechanical systems.
We are proposing a method for identifying whether the observed behaviour of a function at an interface is consistent with the typical behaviour of a particular programming language. This is a challenging problem with significant potential applications such as in security (intrusion detection) or compiler optimisation (profiling). To represent behaviour we use game semantics, a powerful method of semantic analysis for programming languages. It gives mathematically accurate models (‘fully abstract’) for a wide variety of programming languages. Game-semantic models are combinatorial characterisations of all possible interactions between a term and its syntactic context. Because such interactions can be concretely represented as sets of sequences, it is possible to ask whether they can be learned from examples. Concretely, we are using LSTM, a technique which proved effective in learning natural languages for automatic translation and text synthesis, to learn game-semantic models of sequential and concurrent versions of Idealised Algol (IA), which are algorithmically complex yet can be concisely described. We will measure how accurate the learned models are as a function of the degree of the term and the number of free variables involved. Finally, we will show how to use the learned model to perform latent semantic analysis between concurrent and sequential Idealised Algol.
