A logic for the stepwise development of reactive systems

Madeira, Alexandre, Soares Barbosa, Luís, Hennicker, Rolf and Martins, Manuel, (2018). A logic for the stepwise development of reactive systems. Theoretical Computer Science, 744 78-96

Document type:

  • Sub-type Journal article
    Author Madeira, Alexandre
    Soares Barbosa, Luís
    Hennicker, Rolf
    Martins, Manuel
    Title A logic for the stepwise development of reactive systems
    Appearing in Theoretical Computer Science
    Volume 744
    Publication Date 2018-10-05
    Place of Publication Amsterdam
    Publisher Elsevier
    Start page 78
    End page 96
    Language eng
    Abstract [mathematical symbol] is a new dynamic logic combining regular modalities with the binder constructor typical of hybrid logic, which provides a smooth framework for the stepwise development of reactive systems. Actually, the logic is able to capture system properties at different levels of abstraction, from high-level safety and liveness requirements, to constructive specifications representing concrete processes. The paper discusses its semantics, given in terms of reachable transition systems with initial states, its expressive power and a proof system. The methodological framework is in debt to the landmark work of D. Sannella and A. Tarlecki, instantiating the generic concepts of constructor and abstractor implementations by standard operators on reactive components, e.g. relabelling and parallel composition, as constructors, and bisimulation for abstraction.
    Keyword Specification
    Reactive systems
    Dynamic logic
    Hybrid logic
    Copyright Holder Elsevier
    Copyright Year 2018
    Copyright type All rights reserved
    DOI 10.1016/j.tcs.2018.03.004
  • Versions
    Version Filter Type
  • Citation counts
    Google Scholar Search Google Scholar
    Access Statistics: 565 Abstract Views  -  Detailed Statistics
    Created: Fri, 31 Jan 2020, 23:29:59 JST by Mario Peixoto on behalf of UNU EGOV