Trustworthy Systems

Special issue on ``Combining Compositionality and Concurrency'': Part 2

Authors

Rob van Glabbeek, Ursula Goltz and Ernst-Rüdiger Olderog

UNSW

TU Braunschweig

University of Oldenburg
Germany

Abstract

This is the second part of the special issue motivated by the workshop “25 Years of Combining Compositionality and Concurrency” that we organised in August 2013 in Königswinter near Bonn, Germany. The first part was published in Acta Informatica (2015) 52(1):3–106. For an introduction to the topic see our editorial there. This second part comprises four papers.

The paper Richer Interface Automata with Optimistic and Pessimistic Compatibility by Gerald Lüttgen, Walter Vogler, and Sascha Fendrich addresses component-based reasoning for concurrent systems via modal interface automata (MIA). The authors study optimistic and pessimistic MIA variants with internal must-transitions. They define conjunction and disjunction on interfaces as well as mechanisms for extending alphabets.

The paper Compositional Verification of Asynchronous Concurrent Systems using CADP by Hubert Garavel, Frédéric Lang, and Radu Mateescu investigates how various compositional techniques help to fight the state-space explosion in the verification of asynchronous message-passing systems. The techniques are implemented in the toolbox CADP (Construction and Analysis of Distributed Processes). The authors compare the different approaches using a common case study.

The paper Denotational Fixed-Point Semantics for Constructive Scheduling of Synchronous Concurrency by Joaquín Aguado, Michael Mendler, Reinhard von Hanxleden, and Insa Fuhrmann defines an abstract semantic domain and an associated denotational semantics for synchronous programs. The semantics induces three notions of constructiveness, among them the new notion of Input Berry-constructiveness (IBC) for these programs. The authors study behavioural properties of IBC programs.

The paper Compositional Construction of Most General Controllers by Joachim Klein, Christel Baier, and Sascha Klüppelholz considers for given transitions systems conjunctions of linear-time objectives to be achieved by a controller. The authors present game-based algorithms for the compositional construction of most general controllers for invariance, reachability, and ω-regular objectives.

BibTeX Entry

  @inbook{vanGlabbeek_GO_15_2,
    author           = {van Glabbeek, Robert and Goltz, Ursula and Olderog, Ernst-R\"udiger},
    booktitle        = {Acta Informatica},
    editor           = {{Robert van Glabbeek, Ursula Goltz and Ernst-R\"udiger Olderog}},
    keywords         = {concurrency, compositionality, modal interface automata, asynchronous systems, cadp, denotational
                        semantics, synchronous programs, most general controllers},
    month            = jun,
    number           = {4-5},
    pages            = {303--304},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8824.pdf},
    publisher        = {Springer},
    title            = {Special issue on ``{Combining Compositionality and Concurrency}'': part 2},
    volume           = {52},
    year             = {2015}
  }

Download