• DocumentCode
    1832085
  • Title

    An Algebraic System of Temporal Structures

  • Author

    French, Tim ; McCabe-Dansted, John ; Reynolds, Mark

  • Author_Institution
    Sch. of Comput. Sci. & Software Eng., Univ. of Western Australia, Crawley, WA, Australia
  • fYear
    2013
  • fDate
    26-28 Sept. 2013
  • Firstpage
    81
  • Lastpage
    88
  • Abstract
    Lauchli and Leonard, in 1966, described a series of operations which are able to build all linear temporal structures up to first order equivalence. More recently these operations have been used to describe executions of continuous systems for the purposes of model checking real-time specifications. In this paper we present an algebra over these operations and show that it is both sound and complete, in that it can generate all equivalences over these models.
  • Keywords
    algebra; formal specification; formal verification; Lauchli; Leonard; algebraic system; continuous systems; first order equivalence; linear temporal structures; model checking real-time specifications; Algebra; Cognition; Complexity theory; Computational modeling; Continuous time systems; Games; Syntactics; linear structures; model expressions; temporal logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Temporal Representation and Reasoning (TIME), 2013 20th International Symposium on
  • Conference_Location
    Pensacola, FL
  • ISSN
    1530-1311
  • Print_ISBN
    978-1-4799-2240-6
  • Type

    conf

  • DOI
    10.1109/TIME.2013.18
  • Filename
    6786799