Carlos Olarte

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.