arXiv subjects

Bogdan Macovei

Publications and source records attributed to Bogdan Macovei.

4 recordsLinked to original sources

arXiv2026

Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean

We present a Lean formalization of a general hybrid modal logic with many-sorted signatures and polyadic modal operators. The system borrows ideas from both algebraic specification and dynamic logics, and is designed to serve as a uniform axiomatic foundation for specifying and verifying programming languages and security protocols. We expose a DSL for users to define languages and protocols as many-sorted signatures, specify the relevant domain-specific axioms, and reason about program executions or protocol runs. We provide a machine-checked proof of its soundness theorem and showcase the framework's versatility through several applications: an imperative programming language for code verification, the BAN logic for security protocols, and the modal system S5. We have designed our formalization to be intrinsically sorted, that is, well-sorted formulas in the base language are well-typed terms in Lean. Thanks to intrinsic sorting, all domain specific applications can be easily embedded in our framework via the DSL, at no additional syntactic overhead required for the user to prove. All code presented in this paper is openly accessible in the following repository: https://github.com/alexoltean61/msphml-lean

cs.LO↗

arXiv2025

Łukasiewicz Logic with Actions for Neural Networks training

Based on the already known connection between multilayer perceptrons and Lukasiewicz logic with rational coefficients, we take a step forward in analyzing its training process using a three-sorted hybrid modal logic: a multilayer perceptron is a logical formula; the actions of the training process are modal operators; the training process is a sequence of logical deductions. Using the proof assistant and the programming language Lean 4, the algorithmic implementation of the training process is certified by logical proofs.

cs.LO↗

arXiv2023

A Parallel Dynamic Epistemic Perspective over Muddy Children Puzzle

Epistemic protocols represents a current field of interest, with numerous approaches still being studied. In this paper we formalize parallel sessions of the The Muddy Children Puzzle using Public Observation Logic, a system that allows epistemic update. We consider agents with roles in multiple sessions and the information update in all parallel sessions as new information is discovered in any particular session.

cs.LO↗

arXiv2021

DELP: Dynamic Epistemic Logic for Security Protocols

The formal analysis of security protocols is a challenging field, with various approaches being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to validate security protocols. Combining ideas from previous approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of its properties are verifyied, using the theorem prover Lean.

cs.LO↗