My research interests are concurrent systems and formal methods.
I'm also member of the AVISPA research group.
email: carlos.olarte at gmail ... com
- A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets (with J. Arias, K. Bae, P. Ölveczky and L. Petrucci). This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude -- including full LTL model checking, analysis with user-defined analysis strategies, and even statistical model checking -- for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Romeo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Romeo in many cases. (arXiv).
- Optimal Scheduling of Agents in ADTs: Specialised Algorithm and Declarative Models (with J. Arias, L. Petrucci, Łukasz Masko, Wojciech Penczek and Teofil Sidoruk). Expressing attack-defense trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agentsr' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using the minimal number of agents for a given attack-defence tree. We also investigate an alternative approach for the same problem using Rewriting Logic, starting with a simple and elegant declarative model, whose correctness (in terms of schedule's optimality) is self-evident. We then refine this specification, inspired by the design of our specialised algorithm, to obtain an efficient system that can be used as a playground to explore various aspects of attack-defence trees. We compare the two approaches on different benchmarks. Associated tool adt2maude. (PDF).
- A Rewriting Logic Semantics and Statistical Analysis for Probabilistic Event-B (with C. Rocha and D. Osorio). Probabilistic specifications are fast gaining ground as a tool for statistical modeling of probabilistic systems. One of the main goals of formal methods in this domain is to ensure that specific behavior is present or absent in the system, up to a certain confidence threshold, regardless of the way it operates amid uncertain information. This paper presents a rewriting logic semantics for a probabilistic extension of Event-B, a proof-based formal method for discrete systems modeling. The proposed semantics adequately captures the three sources of probabilistic behavior, namely, probabilistic assignments, parameters, and concurrency. Hence, simulation and probabilistic temporal verification become automatically available for probabilistic Event-B models. The approach takes as input a probabilistic Event-B specification, and outputs a probabilistic rewrite theory that is fully executable in PMaude and can be statistically tested against quantitative metrics. The approach is illustrated with examples in the paper. (arXiv).
Recently Accepted Papers
- Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving (with J. Arias, K. Bae, P. Ölveczky, L. Petrucci and F. Rømming). This paper presents a rewriting logic “interpreter” for networks of parametric timed automata with global variables (NPTAVs) in Real-Time Maude style. Since explicit-state analysis is not sound and complete for such dense-time systems, we explain how our real-time rewrite theory can be systematically transformed into a rewrite theory that is amenable to symbolic analysis using the integration of Maude with SMT solving. We show that symbolic reachability analysis using Maude-with-SMT of the resulting rewrite theory is sound and complete for the NPTAV reachability problem. We extend and optimize standard Maude-with-SMT reachability analysis with folding and merging of symbolic states, so that the analysis terminates when the symbolic state space of the NPTAV is finite. These procedures rely on a subsumption relation that requires eliminating existentially quantified SMT variables. We have therefore implemented the Fourier-Motzkin quantifier elimination algorithm, thereby making our rewrite theory executable with any SMT solver connected to Maude. We show how we can provide most reachability and parameter synthesis analysis methods provided by Imitator, a state-of-the-art tool for NPTAVs. We compare the performance of our analysis methods with those of Imitator on a wide range of benchmarks, with the expected outcome. The practical contributions are two-fold: providing new analysis methods for NPTAVs—e.g., allowing more general state properties and supporting reachability analysis combined with user-defined execution strategies—not supported by Imitator, and developing symbolic analysis methods for both real-time rewrite theories and rewrite theories in general. (Scienc of Computer Programming).
- Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving (with J. Arias, K. Bae, P. Ölveczky, L. Petrucci and F. Rømming). Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding approach for symbolic reachability that terminates whenever the parametric state-class graph of the PITPN is finite. We explain how almost all formal analysis and parameter synthesis supported by the state-of-the-art PITPN tool Romeo can be done in Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments on three benchmarks show that our methods outperform Romeo in many cases. To appear in Petri Nets 2023. Extended version and tool here.
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems (with E. Pimentel and C. Rocha). This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-admissibility, and identity expansion. Although undecidable in general, these structural properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms –which take advantage of the rewriting logic meta-logical framework– are explained in detail and illustrated with examples throughout the paper. They have been fully mechanized in the L-Framework, thus offering both a formal specification language and off-the-shelf mechanization of the proof-search algorithms coming together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies in the paper, the L-Framework achieves a great degree of automation when used on several propositional sequent systems, including single conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic and its dyadic system, intuitionistic linear logic, and normal modal logics. To appear in JLAMP. Companion tool: L-Framework.
PITPN2Maude: Rewriting Logic Semantics for parametric time Petri nets with inhibitor arcs (Petri Nets 2023 paper).
RESPEG: Rewriting Semantics for PEGs (SLE'20 paper).
L-Framework: structural proof theory in Maude (WRLA'18 and JLAMP'23 paper).
Slicer for CCP (FI'20 paper).
ESTRO: From Multiparty Session Types to Event-B (SAC'16 paper)
LolliP: Linear CCP interpreter
Alcove: Access Permissions Linear COnstraints VErifier (TPLP'18 paper).
NATO Science for Peace and Security Programme project SymSafe (No. G6133) (2023)
Promueva: Investigación en Modelos Computacionales de Redes Sociales (2022).
Aesir: Timed strAtegies for rEwrite-based Symbolic analysIs of Real-time systems (2022).
ESPRiTS: Extending Synthesis of Parameters to RewrIting Timed (2022).
SÉMANTIQUE : Spécification et vÉrification des systèMes multimédiAs iNteracTifs : une approchebasée sur la logIQue de réecritUrE (2022)
CNPq Bolsa de Produtividade (2019-2022): LOGOCOSMICS: LOgica, joGOs e Cálculos de prOcessos para Sistemas ModaIs ConcorrenteS
CNPq Projeto Universal (2019-2022): Sistemas concorrentes: semântica, provas e modelos declarativos.
EPIC: EPistemic Interactive Concurrency. STIC-AmSud Project. In collaboration with INRIA and Universidad Javeriana Cali. 2017.
MOSAIC - Modalities in Substructural Logics: Theory, Methods and Applications. Sklodowska-Curie Action: RISE Grant Agreement no 101007627.
I'm one of the invited speakers of SynCoP 2024.
I'm member of the publicity committee of SIGLOG.
17th International Symposium on Functional and Logic Programming (FLOPS'24)
15th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'23)
9th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'23)
Co-chair of Logical Frameworks and Meta Languages: Theory and Practice (LFMTP'23).
PC member of the 25th International Symposium on Principles and Practice of Declarative Programming (PPDP'23)
PC member of the 29th Workshop on Logic, Language, Information and Computation (WoLLIC 2023)
PC member of the 33rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'23).
Editor of the area Specification, Analysis and Verification of Systems, Security of the ALP Newsletter.
7th International Conference on Formal Structures for Computation and Deduction (FSCD'22)
8th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'22)
International Conference on Software Language Engineering SLE'2021.
International Conference on Logic Programming ICLP'2021.
Co-chair of WBL'21 (Workshop Brasileiro de Lógica).
16th International Workshop on Logical and Semantic Frameworks, with Applications. LSFA'21.
15th International Workshop on Logical and Semantic Frameworks, with Applications. LSFA'20.
Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020.
35th International Conference on Logic Programming ICLP'19.
27th International Conference on Automated Deduction CADE'27.
29th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR'19.
Sixth Workshop on Proof eXchange for Theorem Proving PxTP 2019.
Co-chair of LSFA'18.
Logical Frameworks and Meta-Languages: Theory and Practice - LFMTP'18.
5th Workshop on Horn Clauses for Verification and Synthesis - HCVS'18.