Completeness and Incompleteness of Synchronous Kleene Algebra
| Autor: | Wagemaker, J., Bonsangue, M., Kappé, T., Rot, J., Silva, A., Hutton, G. |
|---|---|
| Přispěvatelé: | Hutton, G. |
| Rok vydání: | 2019 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science 050101 languages & linguistics Computer science 05 social sciences 02 engineering and technology Extension (predicate logic) Logic in Computer Science (cs.LO) Set (abstract data type) Algebra Kleene algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Regular language TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Completeness (order theory) ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Kleene star Software Science 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Operator product expansion Axiom |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030336356 Lecture Notes in Computer Science Lecture Notes in Computer Science-Mathematics of Program Construction Hutton, G. (ed.), Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019. Proceedings, 385-413. Cham : Springer International Publishing STARTPAGE=385;ENDPAGE=413;ISSN=0302-9743;TITLE=Hutton, G. (ed.), Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019. Proceedings Mathematics of Program Construction-13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings Hutton, G. (ed.), Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019. Proceedings, pp. 385-413 |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-030-33636-3_14 |
| Popis: | Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics. Comment: Accepted at MPC 2019 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|