Towards determinism in PDL: relations and proof theory

Benevides, Mario; Gomes, Leandro; Lopes, Bruno

Document type :

Article dans une revue scientifique: Article original

DOI :

10.1093/logcom/exae022

Permalink :

http://hdl.handle.net/20.500.12210/126903

Title :

Towards determinism in PDL: relations and proof theory

Author(s) :

Benevides, Mario [Auteur]
Universidade Federal Fluminense [Rio de Janeiro] [UFF]
Instituto de Computação [Niteroi-Rio de Janeiro] [IC-UFF]
Gomes, Leandro [Auteur]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Lopes, Bruno [Auteur]
Universidade Federal Fluminense [Rio de Janeiro] [UFF]
Instituto de Computação [Niteroi-Rio de Janeiro] [IC-UFF]

Journal title :

Journal of logic and computation

Publisher :

Oxford University Press (OUP)

Publication date :

2024-05-21

ISSN :

0955-792X

English keyword(s) :

Dynamic logic
GKAT
GPDL

HAL domain(s) :

Informatique [cs]
Mathématiques [math]/Logique [math.LO]

English abstract : [en]

Guarded Kleene Algebra with Tests (GKAT) was presented as a fragment of KAT to abstract imperative programming languages, where only if-then-else and while-do statements are allowed in the language. The loss of expressiveness ...
Show more >Guarded Kleene Algebra with Tests (GKAT) was presented as a fragment of KAT to abstract imperative programming languages, where only if-then-else and while-do statements are allowed in the language. The loss of expressiveness is, nevertheless, compensated by a clear advantage over KAT: it allows almost linear decidability of program equivalence. In this work, we give the first step to optimizing the complexity of dynamic logic equivalence, which is EXPTIME-complete in propositional dynamic logic (PDL). First, and based on strict deterministic PDL, we present guarded propositional dynamic logic (GPDL), a fragment of PDL where programs correspond to GKAT terms. It comes embedded, as expected, with a semantics over relational models and a sound axiomatisation. Then, we present a Natural Deduction system for GPDL, proving its soundness and completeness, concerning the axiomatisation. Based on Smolka et al. (2019, Proceedings of the ACM Programming Language 4), we obtain the main result of this work—the equivalence of GPDL programs can be established in almost linear time.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL

Submission date :

2025-04-09T02:04:09Z

Files

document
Open access
Access the document

2024_Journal_of_Logic_and_Computation.pdf
Open access
Access the document

Towards determinism in PDL: relations and ... BibTeX CSV Excel RIS

Files

Towards determinism in PDL: relations and ...

BibTeX

CSV

Excel

RIS