×

A logic for the stepwise development of reactive systems. (English) Zbl 1400.68125

Summary: \(\mathcal{D}^\downarrow\) 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

CASL
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Aceto, L.; Ingólfsdóttir, A.; Larsen, K. G.; Srba, J., Reactive systems: modelling, specification and verification, (2007), Cambridge University Press · Zbl 1141.68043
[2] Areces, C.; Blackburn, P.; Marx, M., A road-map on complexity for hybrid logics, (Flum, J.; Rodríguez-Artalejo, M., 13th Intern. Workshop Computer Science Logic, CSL’99, Madrid, Spain, September 20-25, 1999, Lecture Notes in Computer Science, vol. 1683, (1999), Springer), 307-321 · Zbl 0942.03048
[3] Astesiano, E.; Bidoit, M.; Kirchner, H.; Krieg-Brückner, B.; Mosses, P. D.; Sannella, D.; Tarlecki, A., CASL: the common algebraic specification language, Theoret. Comput. Sci., 286, 2, 153-196, (2002) · Zbl 1061.68103
[4] Baeten, J. C.M.; Basten, T.; Reniers, M. A., Process algebra: equational theories of communicating processes, (2010), Cambridge University Press · Zbl 1234.68001
[5] Bidoit, M.; Hennicker, R., Constructor-based observational logic, J. Log. Algebr. Program., 67, 1-2, 3-51, (2006) · Zbl 1088.68112
[6] Blackburn, P.; Tzakova, M., Hybrid languages and temporal logic, Log. J. IGPL, 7, 1, 27, (1999) · Zbl 0920.03029
[7] Braüner, T., Hybrid logic and its proof-theory, Appl. Log. Ser., (2010), Springer
[8] Cengarle, M. V., The temporal logic institution, (1998), LUM München, Institut für Informatik, Technical Report Technical Report 9805
[9] Diaconescu, R., Institutional semantics for many-valued logics, Fuzzy Sets and Systems, 218, 32-52, (2013) · Zbl 1307.03014
[10] Fiadeiro, J. L.; Maibaum, T. S.E., Temporal theories as modularisation units for concurrent system specification, Form. Asp. Comput., 4, 3, 239-272, (1992) · Zbl 0746.68031
[11] Goguen, J. A.; Burstall, R. M., Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146, (1992) · Zbl 0799.68134
[12] Goldblatt, R., Logics of time and computation, CSLI Lecture Notes, vol. 7, (1992), Center for the Study of Language and Information Stanford, CA
[13] Goranko, V., Temporal logic with reference pointers, (Gabbay, D. M.; Ohlbach, H. J., First Int. Conf. Temporal Logic, ICTL, Lecture Notes in Computer Science, vol. 827, (1994), Springer), 133-148 · Zbl 0949.03515
[14] Gorrieri, R.; Rensink, A.; Zamboni, M. A., Action refinement, (Handbook of Process Algebra, (2000), Elsevier), 1047-1147 · Zbl 1035.68068
[15] Groote, J. F.; Mousavi, M. R., Modeling and analysis of communicating systems, (2014), MIT Press
[16] Harel, D.; Kozen, D.; Tiuryn, J., Dynamic logic, (2000), MIT Press · Zbl 0976.68108
[17] Havelund, K., The fork calculus—towards a logic for concurrent ML, (1994), DIKU, University of Copenhagen Denmark, PhD thesis
[18] Hennicker, R.; Madeira, A., Observational semantics for the dynamic logic with binders, (Roggenbach, M.; Oliet, N., Recent Trends in Algebraic Development Methods, Lecture Notes in Computer Science, vol. 10644, (2017), Springer), 135-152
[19] Hoare, C. A.R., Proof of correctness of data representations, Acta Inform., 1, 271-281, (1972) · Zbl 0244.68009
[20] Hoare, C. A.R., Communicating sequential processes, Series in Computer Science, (1985), Prentice-Hall International · Zbl 0637.68007
[21] Jones, C. B., Software development — a rigorous approach, Series in Computer Science, (1980), Prentice Hall · Zbl 0424.68019
[22] Knijnenburg, P.; van Leeuwen, J., On models for propositional dynamic logic, Theoret. Comput. Sci., 91, 2, 181-203, (1991) · Zbl 0753.68061
[23] Larsen, K. G.; Thomsen, B., A modal process logic, (Third Annual Symposium on Logic in Computer Science, (1988), IEEE Computer Society), 203-210
[24] Madeira, A.; Barbosa, L. S.; Hennicker, R.; Martins, M. A., Dynamic logic with binders and its application to the development of reactive systems, (Sampaio, A.; Wang, F., Theoretical Aspects of Computing, 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings, ICTAC 2016, Springer Lecture Notes in Computer Science, vol. 9965, (2016)), 422-440 · Zbl 1482.68143
[25] Magee, J.; Kramer, J., Concurrency - state models and Java programs, (2006), Wiley
[26] O’Reilly, L.; Mossakowski, T.; Roggenbach, M., Compositional modelling and reasoning in an institution for processes and data, (Mossakowski, T.; Kreowski, H.-J., WADT 2010, Selected Papers, (2012), Springer), 251-269 · Zbl 1312.68146
[27] Park, D., Concurrency and automata on infinite sequences, (Deussen, P., Theoretical Computer Science, 5th GI-Conference, Lecture Notes in Computer Science, vol. 104, (1981), Springer), 167-183
[28] Reggio, G.; Astesiano, E.; Choppy, C., Casl-ltl: a casl extension for dynamic reactive systems version 1.0. - summary, (2013), DFKI Lab Bremen, Technical report disi-tr-03-36. Technical report
[29] Reisig, W., Petri nets: an introduction, EATCS Monographs on Theoretical Computer Science, (1985), Springer Verlag · Zbl 0555.68033
[30] Roggenbach, M., CSP-CASL - a new integration of process algebra and algebraic specification, Theoret. Comput. Sci., 354, 1, 42-71, (2006) · Zbl 1088.68132
[31] Sannella, D.; Tarlecki, A., Toward formal development of programs from algebraic specifications: implementations revisited, Acta Inform., 25, 3, 233-281, (1988) · Zbl 0621.68004
[32] Sannella, D.; Tarlecki, A., Foundations of algebraic specification and formal software development, Monographs on TCS, an EATCS Series, (2012), Springer · Zbl 1237.68129
[33] Sekerinski, E.; Sere, K., Program development by refinement: case studies using the B method, (2012), Springer Science and Business Media
[34] Winskel, G.; Nielsen, M., Models for concurrency, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 4, (1995), Oxford University Press Oxford, UK), 1-148
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.