Skip to main content
Erschienen in:
Buchtitelbild

2020 | OriginalPaper | Buchkapitel

Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq

verfasst von : Raul Fervari, Francisco Trucco, Beta Ziliani

Erschienen in: Dynamic Logic. New Trends and Applications

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

Over the last years, the study of logics that can modify a model while evaluating a formula has gained in interest. Motivated by many examples in practice such as hybrid logics, separation logics and dynamic epistemic logics, the ability of updating a model has been investigated from a more general point of view. In this work, we formalize and verify in the proof assistant Coq, the bisimulation theorems for a particular family of dynamic logics that can change the accessibility relation of a model. The benefits of this formalization are twofold. First, our results apply for a wide variety of dynamic logics. Second, we argue that this is the first step towards the development of a modal logic library in Coq, which allows us to mechanize many relevant results in modal logics.

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!

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!

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!

Literatur
3.
Zurück zum Zitat Areces, C., Fervari, R., Hoffmann, G.: Relation-changing modal operators. Log. J. IGPL 23(4), 601–627 (2015)MathSciNetCrossRef Areces, C., Fervari, R., Hoffmann, G.: Relation-changing modal operators. Log. J. IGPL 23(4), 601–627 (2015)MathSciNetCrossRef
4.
Zurück zum Zitat Areces, C., Fervari, R., Hoffmann, G., Martel, M.: Satisfiability for relation-changing logics. J. Log. Comput. 28(7), 1443–1470 (2018)MathSciNetCrossRef Areces, C., Fervari, R., Hoffmann, G., Martel, M.: Satisfiability for relation-changing logics. J. Log. Comput. 28(7), 1443–1470 (2018)MathSciNetCrossRef
5.
Zurück zum Zitat Areces, C., Figueira, D., Figueira, S., Mera, S.: The expressive power of memory logics. Rev. Symb. Log. 4(2), 290–318 (2011)MathSciNetCrossRef Areces, C., Figueira, D., Figueira, S., Mera, S.: The expressive power of memory logics. Rev. Symb. Log. 4(2), 290–318 (2011)MathSciNetCrossRef
6.
Zurück zum Zitat Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logic, pp. 821–868. Elsevier, Amsterdam (2007)CrossRef Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logic, pp. 821–868. Elsevier, Amsterdam (2007)CrossRef
7.
Zurück zum Zitat Aucher, G., Balbiani, P., Fariñas del Cerro, L., Herzig, A.: Global and local graph modifiers. ENTCS 231, 293–307 (2009)MathSciNet Aucher, G., Balbiani, P., Fariñas del Cerro, L., Herzig, A.: Global and local graph modifiers. ENTCS 231, 293–307 (2009)MathSciNet
8.
Zurück zum Zitat Aucher, G., van Benthem, J., Grossi, D.: Modal logics of sabotage revisited. JLC 28(2), 269–303 (2018)MathSciNetMATH Aucher, G., van Benthem, J., Grossi, D.: Modal logics of sabotage revisited. JLC 28(2), 269–303 (2018)MathSciNetMATH
9.
Zurück zum Zitat Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010)MATH Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010)MATH
10.
Zurück zum Zitat Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)CrossRef Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)CrossRef
11.
Zurück zum Zitat Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, pp. 1–84. Elsevier (2007) Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, pp. 1–84. Elsevier (2007)
12.
Zurück zum Zitat Bohrer, B., Platzer, A.: Toward structured proofs for dynamic logics. CoRR, abs/1908.05535 (2019) Bohrer, B., Platzer, A.: Toward structured proofs for dynamic logics. CoRR, abs/1908.05535 (2019)
13.
Zurück zum Zitat D’Abrera, C., Goré, R.: Verified synthesis of (very simple) Sahlqvist correspondents via Coq. In: AiML 2018, Short Presentations, pp. 26–30. College Publications (2018) D’Abrera, C., Goré, R.: Verified synthesis of (very simple) Sahlqvist correspondents via Coq. In: AiML 2018, Short Presentations, pp. 26–30. College Publications (2018)
15.
Zurück zum Zitat de Wind, P.: Modal Logic in Coq. Vrije Universiteit, Amsterdam (2001) de Wind, P.: Modal Logic in Coq. Vrije Universiteit, Amsterdam (2001)
16.
Zurück zum Zitat Demri, S., Fervari, R.: On the complexity of modal separation logics. In: AiML 2018, pp. 179–198. College Publications (2018) Demri, S., Fervari, R.: On the complexity of modal separation logics. In: AiML 2018, pp. 179–198. College Publications (2018)
18.
Zurück zum Zitat Fervari, R.: Relation-Changing Modal Logics. Ph.D. thesis, Universidad Nacional de Córdoba, Argentina (2014) Fervari, R.: Relation-Changing Modal Logics. Ph.D. thesis, Universidad Nacional de Córdoba, Argentina (2014)
20.
Zurück zum Zitat Fervari, R., Velázquez-Quesada, F.R.: Introspection as an action in relational models. JLAMP 108, 1–23 (2019)MathSciNetMATH Fervari, R., Velázquez-Quesada, F.R.: Introspection as an action in relational models. JLAMP 108, 1–23 (2019)MathSciNetMATH
21.
Zurück zum Zitat Girard, P., Seligman, J., Liu, F.: General dynamic dynamic logic. In: AiML 2012, pp. 239–260. College Publications (2012) Girard, P., Seligman, J., Liu, F.: General dynamic dynamic logic. In: AiML 2012, pp. 239–260. College Publications (2012)
22.
Zurück zum Zitat Gonthier, G.: Formal proof – the four-color theorem (2008) Gonthier, G.: Formal proof – the four-color theorem (2008)
24.
Zurück zum Zitat Harel, D.: Dynamic Logic. Foundations of Computing. The MIT Press, Cambridge (2000)CrossRef Harel, D.: Dynamic Logic. Foundations of Computing. The MIT Press, Cambridge (2000)CrossRef
25.
Zurück zum Zitat Howard, W.A.: The formulae-as-types notion of construction. To HB Curry: Essays Combin. Log. Lambda Calc. Formalism 44, 479–490 (1980) Howard, W.A.: The formulae-as-types notion of construction. To HB Curry: Essays Combin. Log. Lambda Calc. Formalism 44, 479–490 (1980)
26.
Zurück zum Zitat Kripke, S.: Semantical analysis of modal logic I. Normal propositional calculi. Z. fur Math. Log. Grundlagen der Math. 9, 67–96 (1963)MathSciNetCrossRef Kripke, S.: Semantical analysis of modal logic I. Normal propositional calculi. Z. fur Math. Log. Grundlagen der Math. 9, 67–96 (1963)MathSciNetCrossRef
28.
Zurück zum Zitat Mitsch, S., Platzer, A.: The keymaera X proof IDE - concepts on usability in hybrid systems theorem proving. In: F-IDE@FM 2016. EPTCS, vol. 240, pp. 67–81 (2016)CrossRef Mitsch, S., Platzer, A.: The keymaera X proof IDE - concepts on usability in hybrid systems theorem proving. In: F-IDE@FM 2016. EPTCS, vol. 240, pp. 67–81 (2016)CrossRef
30.
Zurück zum Zitat Pym, D., Spring, J., O’Hearn, P.W.: Why separation logic works. Philos. Technol. 32(3), 483–516 (2019)CrossRef Pym, D., Spring, J., O’Hearn, P.W.: Why separation logic works. Philos. Technol. 32(3), 483–516 (2019)CrossRef
31.
Zurück zum Zitat Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE (2002) Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE (2002)
32.
Zurück zum Zitat Rohde, P.: On games and logics over dynamically changing structures. Ph.D. thesis, RWTH Aachen (2006) Rohde, P.: On games and logics over dynamically changing structures. Ph.D. thesis, RWTH Aachen (2006)
35.
Zurück zum Zitat van Benthem, J., Liu, F.: Dynamic logic of preference upgrade. J. Appl. Non-Class. Log. 17(2), 157–182 (2007)MathSciNetCrossRef van Benthem, J., Liu, F.: Dynamic logic of preference upgrade. J. Appl. Non-Class. Log. 17(2), 157–182 (2007)MathSciNetCrossRef
36.
Zurück zum Zitat van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic epistemic logic with assignment. In: AAMAS 2005, pp. 141–148. ACM (2005) van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic epistemic logic with assignment. In: AAMAS 2005, pp. 141–148. ACM (2005)
38.
Zurück zum Zitat Wu, M., Goré, R.: Verified decision procedures for modal logics. In: ITP 2019. LIPIcs, vol. 141, pp. 31:1–31:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019) Wu, M., Goré, R.: Verified decision procedures for modal logics. In: ITP 2019. LIPIcs, vol. 141, pp. 31:1–31:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
39.
Zurück zum Zitat Xavier, B., Olarte, C., Reis, G., Nigam, V.: Mechanizing focused linear logic in Coq. ENTCS 338, 219–236 (2018)MathSciNetMATH Xavier, B., Olarte, C., Reis, G., Nigam, V.: Mechanizing focused linear logic in Coq. ENTCS 338, 219–236 (2018)MathSciNetMATH
Metadaten
Titel
Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq
verfasst von
Raul Fervari
Francisco Trucco
Beta Ziliani
Copyright-Jahr
2020
DOI
https://doi.org/10.1007/978-3-030-38808-9_1