nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions

verfasst von : Rolf Hennicker, Alexander Knapp, Alexandre Madeira, Felix Mindt

Erschienen in: Dynamic Logic. New Trends and Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We extend dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations of the logic: abstractor and behavioural specifications. Abstractor specifications relax the standard model class semantics of a specification by considering its closure under weak bisimulation. Behavioural specifications, however, rely on a behavioural satisfaction relation which relaxes the interpretation of state variables and the satisfaction of modal formulas \(\langle \alpha \rangle \varphi \) and \([\alpha ]\varphi \) by abstracting from silent transitions. A formal relation between abstractor and behavioural specifications is provided which shows that both coincide semantically under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq

Nächstes Kapitel The Logic of AGM Learning from Partial Observations

In general there could be other axioms as well specifying, e.g., disallowed behaviours.

It may sound strange that ordinary satisfaction does not always imply behavioural satisfaction but there are indeed some cases where this can happen; see Example 6.

Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Sci. Comput. Program. 25(2–3), 149–186 (1995)MathSciNetCrossRef

Braüner, T.: Hybrid Logic and its Proof-Theory. Applied Logic Series. Springer, Heidelberg (2010). https://doi.org/10.1007/978-94-007-0002-4CrossRefMATH

Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)CrossRef

Hennicker, R.: Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Asp. Comput. 3(4), 326–345 (1991)CrossRef

Hennicker, R., Madeira, A.: Observational semantics for dynamic logic with binders. In: James, P., Roggenbach, M. (eds.) WADT 2016. LNCS, vol. 10644, pp. 135–152. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72044-9_10CrossRef

Hennicker, R., Madeira, A., Knapp, A.: A hybrid dynamic logic for event/data-based systems. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 79–97. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_5CrossRef

Hennicker, R., Madeira, A., Wirsing, M.: Behavioural and abstractor specifications revisited. Theor. Comput. Sci. 741, 32–43 (2018)MathSciNetCrossRef

Hofmann, M., Sannella, D.: On behavioural abstraction and behavioural satisfaction in higher-order logic. Theor. Comput. Sci. 167(1&2), 3–45 (1996)MathSciNetCrossRef

Madeira, A., Barbosa, L.S., Hennicker, R., Martins, M.A.: Dynamic logic with binders and its application to the development of reactive systems. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 422–440. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_24CrossRefMATH

10.

Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATH

11.

Misiak, M.: Behavioural semantics of algebraic specifications in arbitrary logical systems. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 144–161. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31959-7_9CrossRefMATH

12.

Nivela, M.P., Orejas, F.: Initial behaviour semantics for algebraic specifications. In: Sannella, D., Tarlecki, A. (eds.) ADT 1987. LNCS, vol. 332, pp. 184–207. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-50325-0_10CrossRef

13.

Reichel, H.: Behavioural equivalence – a unifying concept for initial and final specifications. In: Arato, M., Varga, L. (eds.) In: Proceedings of the 3rd Hungarian Computer Science Conference, pp. 27–39. Akademiai Kiado (1981)

14.

Reichel, H.: Behavioural validity of conditional equations in abstract data types. In: Proceedings of the 3rd Vienna Conference Contributions to General Algebra, pp. 301–324. B.G. Teubner (1985)

15.

Sannella, D., Tarlecki, A.: On observational equivalence and algebraic specification. J. Comput. Syst. Sci. 34(2–3), 150–178 (1987)MathSciNetCrossRef

16.

Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation extended abstract. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 413–427. Springer, Heidelberg (1983). https://doi.org/10.1007/3-540-12689-9_122CrossRef

17.

Stirling, C.: Modal and Temporal Properties of Processes. Springer, New York (2001)CrossRef

Titel: Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions
verfasst von: Rolf Hennicker
Alexander Knapp
Alexandre Madeira
Felix Mindt
Verlag: Springer International Publishing
Buch: Dynamic Logic. New Trends and Applications
Print ISBN: 978-3-030-38807-2

Electronic ISBN: 978-3-030-38808-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-38808-9_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"