Search

The Theory of Sequential Processes includes deadlock, successful termination, action prefixing, alternative and sequential composition. Intermediate acceptance, which is important for the integration of classical automata theory, can be expressed through a combination of alternative composition and successful termination. Recently, it was argued that complications arising from the interplay between intermediate acceptance and sequential composition can be eliminated by replacing sequential composition by sequencing. In this paper we study the equational theory of the recursion-free fragment of the resulting process theory modulo bisimilarity, proving that it is not finitely based, but does afford a ground-complete axiomatisation if a unary auxiliary operator is added. Furthermore, we prove that bisimilarity is decidable for processes definable by means of a finite guarded recursive specification over the process theory.

LIPIcs, Volume 139, CALCO'19, Complete Volume, LIPIcs, Vol. 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), pages 0-0

The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies. The DTU/Bremen research has been funded by the RobustRailS project granted by Innovation Fund Denmark. The Surrey/Swansea research has been funded by the SafeCap and the DITTO research projects granted by EPSRC and RSSB. The authors would like to thank Linh Hong Vu for providing the benchmark of scheme plans and the drawings of the track plans.

We present an institution for UML state machines without hierarchical states. The interaction with UML class diagrams is handled via institutions for guards and actions, which provide dynamic components of states (such as valuations of attributes) but abstract away from details of class diagrams. We also study a notion of interleaving product, which captures the interaction of several state machines. The interleaving product construction is the basis for a semantics of composite structure diagrams, which can be used to specify the interaction of state machines. This work is part of a larger effort to build a framework for formal software development with UML, based on a heterogeneous approach using institutions., Comment: 24 pages. arXiv admin note: substantial text overlap with arXiv:1403.7747

CSP-CASL is but one of the many languages for which Bernd Krieg-Brueckner (BKB) had a great deal of influence throughout its development process: from the initial idea of working towards an integration of the process algebra CSP with the algebraic specification language CASL, to the design of the concrete syntax, and also to tool support for CSP-CASL, where the theorem prover Isabelle should provide the common platform. In all this, BKB provided inspiration and guidance, funding, and also a helping hand when needed. This paper provides a survey on the technology developed so far for CSP-CASL, covering results of a theoretical nature, an industrial case study, theorem proving support as well as a testing approach. In honour of BKB’s 60th birthday, this survey documents what has become out of one of BKB’s visions., Electronic Communications of the EASST, Volume 62: Specification, Transformation, Navigation - Special Issue Dedicated to Bernd Krieg-Brückner

Lossy channel systems (LCSs for short) are models for communicating systems where the subprocesses are linked via unbounded FIFO channels which might lose messages. Link protocols, such as the Alternating Bit Protocol and HDLC can be modelled with these systems. The decidability of several verification problems of LCSs has been investigated by Abdulla & Jonsson [AJ93,AJ94], e.g. they have shown that the reachability problem for LCSs is decidable while LT L model checking is not. In this paper, we consider probabilistic LCSs (which are LCSs where the transitions are augmented with appropriate probabilities) as introduced by [IN97] and show that the question of whether or not a linear time property holds with probability 1 is deddable. More precisely, we show how LT L\x model checking for (certain types of) probabilistic LCSs can be reduced to a reachability problem in a (non-probabilistic) LCS where the latter can be solved with the methods of [AJ93].

Bisimulation wurde von Milner (1980) und Park (1981) auf Transitionssystemen eingefuehrt, um Prozesse zu identifizieren, die aus Sicht eines externen Beobachters nicht zu unterscheiden sind. Ausgehend von dieser Idee werden neue Bisimulationsbegriffe auch auf anderen Modellen parallelen Rechnens betrachtet, deren Definition von der Syntax her der urspruenglichen Definition von Bisimulation zumeist aehnlich sieht. Daraus erwaechst die Fragestellung: Was haben diese neuen Bisimulationen mit dem urspruenglichen Begriff zu tun, gibt es mehr als einen nur syntaktischen Zusammenhang zwischen ihnen, laesst sich ein gemeinsamer Ueberbegriff, eine abstrakte Charakterisierung finden? In der Literatur finden sich verschiedene Ansaetze fuer eine abstrakte Charakterisierung von Bisimulation: Degano, De Nicola und Montanari (1993) verwenden spezielle Baeume, Malacaria (1995) arbeitet mit Methoden der Algebra, Aczel und Mendler (1989) einerseits und Joyal, Nielsen und Winskel (1994) andereseits nutzen Begriffe der Kategorientheorie. Wir vergleichen in dieser Arbeit die beiden letztgenannten Ansaetze. Zum einen suchen wir nach direkten Zusammenhaengen zwischen den abstrakten Charakterisierungen. Zum anderen fragen wir uns, ob sich konkrete Bisimulationen auf unterschiedlichen Modellen parallelen Rechnens mittels der abstrakten Charakterisierungen darstellen lassen. Beide Vergleiche lassen den Schluss zu, dass die Charakterisierung von Aczel von den untersuchten Konzepten das umfassendste ist. Von daher beantworten wir die Frage, was eine Bisimulation ist, mit dem Begriff der AM-Bisimulation: Eine Bisimulation zwischen zwei Objekten ist ein Transitionssystem, welches das beobachtbare "Verhalten" wiedergibt, das beiden Objekten gemeinsam ist.

The realm of approaches to operational descriptions and equivalences for concurrent systems in the literature leads to aseries of different attempts to give a uniform characterization of what should be considered as abisimulation, mostly in an algebraic and/or categorical framework. Meanwhile the realm of such approaches calls itselffor comparison and/or unification. We investigate how different abstract characterizations of bisimulations are related and how suitable they are to encompass the various concrete notions of bisimulation.

[AM89] and [JNW94] present abstract concepts of bisimulation in terms of category theory. This paper deals with the question how these approaches are related. Futheron it shows how different types of bisimulations on prime event structures can be modelled in terms of the abstract concepts.

Aczel89 and Joyal94 give distinct characterizations of bisimulation on labelled transition systems in terms of category theory. This paper discusses the differences between their formalisms and shows how to translate these approaches into one another.

This paper adds the technique of chain completion to the setting of [MCB94]. We develop the theory of chain completion Ch(D) of a domain D and show how this completion relates to metric and ideal completion. Especially we study consistency results for denotational semantics on D, Ch(D) and Idl(D).

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop's basic process algebra (BPA) with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based. © 2006 Elsevier B.V. All rights reserved.

In this article the verification and validation of interlocking systems is investigated. Reviewing both geographical and route-related interlocking, the verification objectives can be structured from a perspective of computer science into (1) verification of static semantics, and (2) verification of behavioural (operational) semantics. The former checks that the plant model – that is, the software components reflecting the physical components of the interlocking system – has been set up in an adequate way. The latter investigates trains moving through the network, with the objective to uncover potential safety violations. From a formal methods perspective, these verification objectives can be approached by theorem proving, global, or bounded model checking. This article explains the techniques for application of bounded model checking techniques, and discusses their advantages in comparison to the alternative approaches.