Carlos Olarte

Publications

My list of publications is available in DBLP and ORCID. Some pre-printed version are available here.    

Drafts

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