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:
Article
Collection:
-
Sub-type Journal article Author Madeira, Alexandre
Soares Barbosa, Luís
Hennicker, Rolf
Martins, ManuelTitle 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 logicCopyright Holder Elsevier Copyright Year 2018 Copyright type All rights reserved DOI 10.1016/j.tcs.2018.03.004 -
Citation counts Search Google Scholar
Access Statistics: 507 Abstract Views - Detailed Statistics Created: Fri, 31 Jan 2020, 23:29:59 JST by Mario Peixoto on behalf of UNU EGOV