Expressing iterative properties logically in a symbolic setting

Carron Shankland, Jeremy Bryans, Lionel Morel

    Research output: Chapter in Book/Report/Conference proceedingConference proceeding

    Abstract

    We present a logic for reasoning about state transition systems (LOTOS behaviours) which allows properties involving repeated patterns over actions and data to be expressed. The state transition systems are derived from LOTOS behaviours; however, the logic is applicable to any similar formalism. The semantics of the logic is given with respect to symbolic transition systems, allowing reasoning about data to be separated from reasoning about flow of control. Several motivational examples are included.
    Original languageEnglish
    Title of host publication Algebraic Methodology and Software Technology
    EditorsCharles Rattray, Savitri Maharaj, Carron Shankland
    Place of PublicationBerlin
    Pages460-474
    Number of pages15
    Volume3116
    ISBN (Electronic)978-3-540-27815-3
    DOIs
    Publication statusPublished - 2004

    Keywords

    • LOTOS
    • formal verification
    • temporal logics
    • infinite state systems
    • symbolic representation

    Fingerprint Dive into the research topics of 'Expressing iterative properties logically in a symbolic setting'. Together they form a unique fingerprint.

  • Cite this

    Shankland, C., Bryans, J., & Morel, L. (2004). Expressing iterative properties logically in a symbolic setting. In C. Rattray, S. Maharaj, & C. Shankland (Eds.), Algebraic Methodology and Software Technology (Vol. 3116, pp. 460-474). Berlin. https://doi.org/10.1007/978-3-540-27815-3_35