Carlos Olarte
I'm associate professor at LIPN, Institut Galilée, UMR CNRS 7030, Université Sorbonne Paris Nord. I'm currently on leave from ECT UFRN, Natal (Brazil).
My research interests are concurrent systems and formal methods.
I'm also member of the AVISPA research group.
email: carlos.olarte at gmail.com
Publications
My list of publications is available in DBLP and ORCID. Some pre-printed version are available here.
Drafts
- 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 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.
- Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata (with J. Arias, K. Bae, P. Ölveczky, L. Petrucci and F. Rømming). This paper presents a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs---e.g. allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies---not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories. To appear in Proc. of FTSCS'22. Extended version in HAL and tool PTA2Maude).
- A linear logic framework for multimodal logics (with B. Xavier and E. Pimentel). One of the most fundamental properties of a proof system is analyticity, expressing the fact that a proof of a given formula F only uses subformulas of F. In sequent calculus, this property is usually proved by showing that the cut rule is admissible, i.e., the introduction of the auxiliary lemma H in the reasoning “if H follows from G and F follows from H, then F follows from G” can be eliminated. The proof of cut admissibility is usually a tedious, error-prone process through several proof transformations, thus requiring the assistance of (semi-)automatic procedures. In a previous work by Miller and Pimentel, linear logic ( LL ) was used as a logical framework for establishing sufficient conditions for cut admissibility of object logical systems (OL). The OL’s inference rules are specified as an LL theory and an easy-to-verify criterion sufficed to establish the cut-admissibility theorem for the OL at hand. However, there are many logical systems that cannot be adequately encoded in LL , the most symptomatic cases being sequent systems for modal logics. In this paper, we use a linear-nested sequent ( LNS ) presentation of MMLL (a variant of LL with subexponentials), and show that it is possible to establish a cut-admissibility criterion for LNS systems for (classical or substructural) multimodal logics. We show that the same approach is suitable for handling the LNS system for intuitionistic logic. To appear in Mathematical Structures in Computer Science (MSCS). Formalization in Coq available.
- 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.
Tools
PTA2Maude: Rewriting Logic Semantics for Parametric Timed Automata (FTSCS'22 paper)
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).
A Focused Linear Logical Framework and its Application to Metatheory of Object Logics (Submitted to MSCS).
Benchmarks for intuitionistic linear logic and provers (Linearity & TLLA'18 paper).
Formalizing (First Order) Linear Logic (cut-elimination + focusing) in Coq (LSFA'17 paper).
Prover for Simply Dependent Multimodal Linear Systems (LPAR-21 paper).
SiLVer: Symbolic links verifier (FI'20 paper). A web interface is available here.
Prover for Full Lambek Calculus with Weakening and Bounded Contraction (LSFA'17 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).
Projects
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.
PC Committees and others
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.
I'm member of the publicity committee of SIGLOG.
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.