Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/43346
Título: | Dynamic logic with binders and its application to the development of reactive systems |
Autor(es): | Madeira, Alexandre Leite Castro Barbosa, L. S. Hennicker, Rolf Martins, Manuel A. |
Data: | 2016 |
Editora: | Springer Verlag |
Revista: | Lecture Notes in Computer Science |
Resumo(s): | This paper introduces a logic to support the specification and development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. This is achieved by combining binders of hybrid logic with regular modalities of dynamic logics in the same formalism, which we call D↓-logic. The semantics of our logic focuses on effective processes and is therefore given in terms of reachable transition systems with initial states. The second part of the paper resorts to this logic to frame stepwise development of reactive systems within the software development methodology proposed by Sannella and Tarlecki. In particular, we instantiate the generic concepts of constructor and abstractor implementations by using standard operators on reactive components, like relabelling and parallel composition, as constructors, and bisimulation for abstraction. We also study vertical composition of implementations which relies on the preservation of bisimularity by the constructions on labeleld transition systems. |
Tipo: | Artigo em ata de conferência |
Descrição: | Publicado em "Theoretical aspects of computing - ICTAC 2016: 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings". ISBN 978-3-319-46749-8 |
URI: | https://hdl.handle.net/1822/43346 |
ISBN: | 9783319467498 |
DOI: | 10.1007/978-3-319-46750-4_24 |
ISSN: | 0302-9743 |
Versão da editora: | http://link.springer.com/chapter/10.1007%2F978-3-319-46750-4_24 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
MBHM16.pdf | 527,7 kB | Adobe PDF | Ver/Abrir |