View in EDS

Algebras of modal operators and partial correctness

Saved in:
Bibliographic Details
Title: Algebras of modal operators and partial correctness
Authors: Möller, Bernhard1 moeller@informatik.uni-augsburg.de, Struth, Georg2 struth@informatik.unibw-muenchen.de
Source: Theoretical Computer Science. Feb2006, Vol. 351 Issue 2, p221-239. 19p.
Subjects: Galois theory, Hoare logic, Mathematical logic, Algebra
Abstract: Abstract: Modal Kleene algebras are Kleene algebras enriched by forward and backward box and diamond operators. We formalise the symmetries of these operators as Galois connections, complementarities and dualities. We study their properties in the associated operator algebras and show that the axioms of relation algebra are theorems at the operator level. Modal Kleene algebras provide a unifying semantics for various program calculi and enhance efficient cross-theory reasoning in this class, often in a very concise pointfree style. This claim is supported by novel algebraic soundness and completeness proofs for Hoare logic and by connecting this formalism with an algebraic decision procedure. [Copyright &y& Elsevier]
Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 19592079
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Algebras of modal operators and partial correctness
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Möller%2C+Bernhard%22">Möller, Bernhard</searchLink><relatesTo>1</relatesTo><i> moeller@informatik.uni-augsburg.de</i><br /><searchLink fieldCode="AR" term="%22Struth%2C+Georg%22">Struth, Georg</searchLink><relatesTo>2</relatesTo><i> struth@informatik.unibw-muenchen.de</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Theoretical+Computer+Science%22">Theoretical Computer Science</searchLink>. Feb2006, Vol. 351 Issue 2, p221-239. 19p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Galois+theory%22">Galois theory</searchLink><br /><searchLink fieldCode="DE" term="%22Hoare+logic%22">Hoare logic</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+logic%22">Mathematical logic</searchLink><br /><searchLink fieldCode="DE" term="%22Algebra%22">Algebra</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Abstract: Modal Kleene algebras are Kleene algebras enriched by forward and backward box and diamond operators. We formalise the symmetries of these operators as Galois connections, complementarities and dualities. We study their properties in the associated operator algebras and show that the axioms of relation algebra are theorems at the operator level. Modal Kleene algebras provide a unifying semantics for various program calculi and enhance efficient cross-theory reasoning in this class, often in a very concise pointfree style. This claim is supported by novel algebraic soundness and completeness proofs for Hoare logic and by connecting this formalism with an algebraic decision procedure. [Copyright &y& Elsevier]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=19592079
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.tcs.2005.09.069
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 19
        StartPage: 221
    Subjects:
      – SubjectFull: Galois theory
        Type: general
      – SubjectFull: Hoare logic
        Type: general
      – SubjectFull: Mathematical logic
        Type: general
      – SubjectFull: Algebra
        Type: general
    Titles:
      – TitleFull: Algebras of modal operators and partial correctness
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Möller, Bernhard
      – PersonEntity:
          Name:
            NameFull: Struth, Georg
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 21
              M: 02
              Text: Feb2006
              Type: published
              Y: 2006
          Identifiers:
            – Type: issn-print
              Value: 03043975
          Numbering:
            – Type: volume
              Value: 351
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Theoretical Computer Science
              Type: main
ResultId 1