Please use this identifier to cite or link to this item:
Title: A logic for the stepwise development of reactive systems
Author: Madeira, Alexandre
Barbosa, Luís S.
Hennicker, Rolf
Martins, Manuel A.
Keywords: Dynamic logic
Hybrid logic
Reactive systems
Issue Date: 5-Oct-2018
Publisher: Elsevier
Abstract: D↓ 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
Peer review: yes
DOI: 10.1016/j.tcs.2018.03.004
ISSN: 0304-3975
Appears in Collections:CIDMA - Artigos
AGG - Artigos

Files in This Item:
File Description SizeFormat 
A logic for the stepwise development of reactive systems.pdf543.81 kBAdobe PDFView/Open

Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.