Non-associative Kleene algebra and temporal logics

  • In earlier papers we have presented algebraic semantics of CTL and CTL*. However, they were not fully satisfactory. In particular, the treatment of the iteration operators U ("Until") and W ("While") employed ad-hoc definitions with general recursion, and their interrelation in CTL* and CTL was not set up in a very algebraic way. In this paper we use a new operator with which U and W can be described by variants of the Kleene star and omega iteration. However, the operator is neither associative nor does it have a neutral element. Therefore we present a general investigation of the star and omega for such operators in what we call iteration algebras. The relation between various semantics for CTL* and CTL can then be expressed by homomorphisms between iteration algebras, which is more satisfactory than the original approach.

Download full text files

Export metadata

Statistics

Number of document requests

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Bernhard MöllerGND, Jules DesharnaisGND
URN:urn:nbn:de:bvb:384-opus4-39164
Frontdoor URLhttps://opus.bibliothek.uni-augsburg.de/opus4/3916
Series (Serial Number):Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg (2016-08)
Publisher:Institut für Informatik, Universität Augsburg
Place of publication:Augsburg
Type:Report
Language:English
Publishing Institution:Universität Augsburg
Release Date:2016/12/20
Tag:temporal logics; semantics; Kleene algebra; iteration algebra
Institutes:Fakultät für Angewandte Informatik
Fakultät für Angewandte Informatik / Institut für Informatik
Fakultät für Angewandte Informatik / Institut für Informatik / Professur für Programmiermethodik und Multimediale Informationssysteme
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):Deutsches Urheberrecht mit Print on Demand

OPUS4 Logo