Abstract 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.

Petri Nets are a widely used formalism to deal with concurrent systems. Dynamic Logics (DLs) are a family of modal logics where each modality corresponds to a program. Petri-PDL is a logical language that combines these two approaches: it is a dynamic logic where programs are replaced by Petri Nets. In this work we present a clausal resolution-based calculus for Petri-PDL. Given a Petri-PDL formula, we show how to obtain its translation into a normal form to which a set of resolution-based inference rules are applied. We show that the resulting calculus is sound, complete, and terminating. Some examples of the application of the method are also given.

The amount of available urban data has been increasing over the last years which leaded to new research challenges on Smart Cities domain. Verifying and certifying systems in this domain is one of the challenges that still require some effort. Smart Cities models may be seen as Cyber-Physical Systems and they may be formalized as Finite State machines. Logic-based systems makes possible to take advantage of a wide framework for formally verify this domain. Proof assistants are logic based computational tools developed to mechanize the construction of proofs and Coq, among others, plays an essential role in software validation. This work is tailored to show a way to reason over these models as Finite State machines formalized in the Coq proof assistant from which it is possible to provide certified software to the Smart Cities domain.