Modal kleene algebra and applications a survey département d

Sujets

• informatique
• Marketing et communication

Informations

• Publié par: oeufdepaques
• Nombre de lectures: 147
• Langue: Français

Extrait

      FACULTÉ DES SCIENCES ET DE GÉNIE Département d’informatique et génie logiciel Pavillon Adrien-Pouliot, local 3908 Cité universitaire Québec, Canada G   1K 7P4

 

  MODAL KLEENE ALGEBRA AND APPLICATIONS A SURVEY   PAR   JULES DESHARNAIS, BERNHARD MÖLLER ET GEORG STRUTH     RAPPORT DE RECHERCHE DIUL-RR-0401  

              DÉPARTEMENT D’INFORMATIQUE ET DE GÉNIE LOGICIEL FACULTÉ DES SCIENCES ET DE GÉNIE          

 

Pavillon Adrien-Pouliot Université Laval Sainte-Foy, Québec, Canada G1K 7P4         MARS 2004

Copyright

 c

JulesDesharnais,BernhardMo¨lleretGeorgStruth De´partementd’informatiqueetdeg´enielogiciel Universite Laval ´ Qu´ebecQCG1K7P4 Canada http://www.ift.ulaval.ca —tousdroitsre´serve´s—

Modal Kleene Algebra and Applications — A Survey

Jules Desharnais 1 erdMarll¨oBhnre 2 Georg Struth 2 1 feonrimealtoigqiumeenettdd’eign´e´Dvspretriaee´ticleU,invaLal, Qu´ebecQCG1K7P4Canada [e-mail] 2 bsru,gtstinIikatrmfoInurf¨utguAta¨tisrevinU, Universit¨atsstr.14,D-86135Augsburg,Germany {moeller,struth}@informatik.uni-augsburg.de

AbstractModal Kleene algebras are Kleene algebras with forward and backward modal op- erators defined via domain and codomain operations. They provide a concise and convenient algebraic framework that subsumes various other calculi and allows treating quite a variety of ar- eas. We survey the basic theory and some prominent applications. These include, on the system semantics side, Hoare logic and PDL (Propositional Dynamic Logic),wpcalculus and predicate transformer semantics, temporal logics and termination analysis of rewrite and state transi- tion systems. On the derivation side we apply the framework to game analysis and greedy-like algorithms.

1 Introduction Kleene algebras are fundamental structures in computer science, with applications rang- ing from program development and analysis to rewriting theory and concurrency control. Initially conceived as algebras of regular events [28], they have recently been extended in sev- eral directions. The first direction includes omega algebra, which is a Kleene algebra with an additional operator for infinite iteration [8], demonic refinement algebra [51] and lazy Kleene algebra [33]. The second direction adds tests to Kleene algebra [29]. This allows reasoning about regular programs. All these variants are similar to relational reasoning. Most of them offer a nice balance between economy in concepts and proofs and algorithmic power. The equational theory of Kleene algebra, for instance, can be decided by automata. The third direction, in contrast, is modal in spirit. Here Kleene algebra is combined with a Boolean algebra in a module-based approach [17], the scalar product modelling the application of a modal operator to a state. This yields a calculus that is very similar to certain algebraic approaches to propositional dynamic logics. The modal and the relational approaches to reasoning about programs and state tran- sition systems have been reconciled in Kleene algebra with domain [12]. The three simple equational domain axioms open a new door: they allow the definition of modal operators se- mantically via abstract image and preimage operations. But expressions that mention modal- ities can still in many cases be reduced to pure Kleene algebra with tests. This preserves the algorithmic power of the latter and also provides a very symmetric approach to reasoning about actions and propositions or transitions and states. Compared with relation algebra, modal Kleene algebra does not need the full power of a complete Boolean algebra as the car- rier set, of full additivity of sequential composition, of a converse operation and of residuation; it can make do with very lean versions of these concepts only. In this survey, we discuss modal Kleene algebras both from the theoretical and the practical point of view. On the theoretical side, we introduce the main concepts and review the most important facets of a calculus. Modal Kleene algebras are mathematically quite simple: for actions, they provide only the regular operations of addition, multiplication and reflexive transitive closure; for propositions we have a Boolean algebra. Through their combination via modalities, they become expressive enough for a variety of applications. We also try to point