arXiv subjects

Carlos Olarte

Publications and source records attributed to Carlos Olarte.

At least 19 recordsLinked to original sources

arXiv2026

Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems

The formal analysis of real-time systems must address two dimensions of infiniteness: an unbounded number of agents and messages, and a potentially infinite state space induced by dense time. We present a novel narrowing-based verification method that deals with both dimensions. Our approach integrates (i) rewriting modulo SMT for symbolic representation of timing constraints, (ii) narrowing with logical variables to reason about systems with an unknown number of agents, and (iii) a constraint store over partially instantiated terms, in the style of constraint logic programming. We further introduce a folding mechanism that, under certain conditions, ensures termination of the symbolic analysis. The method has been implemented as an extension of the Maude rewriting engine. We evaluate the approach by verifying the correctness of a timed mutual exclusion protocol without imposing bounds on the number of participating processes. Moreover, we show that the framework uniformly supports the analysis of other real-time models, including parametric timed automata with unspecified components that our method can synthesize. Our results suggest that the proposed framework provides a sound and expressive basis for the symbolic verification of real-time rewrite theories.

cs.SC↗

arXiv2026

Collusion Relations and their Applications to Balance Theory

We study quadrangular properties of binary relations on a set X -i.e., properties defined on configurations of four elements -- within an agonistic interpretation, where xRy is interpreted as x "attacks" y. Such relations induce a suitable notion of "protection," and we provide necessary and sufficient conditions for this notion to be consistent. We characterize the balance property in signed frames in terms of a specific quadrangular property, namely collusivity. In this way, we generalize a classical result in balance theory by offering an alternative method for determining whether a network is polarized. That is, one can identify well-formed groups of agents that agree with one another within the same group (a set of allies) while disagreeing with, or attacking, agents outside the group. Furthermore, we extend the balance theorem to non-symmetric relations, thereby relaxing a condition required in standard balance theory. We conclude by giving a modal characterization of collusive frames, together with corresponding rules in a labeled sequent calculus, and we show that previous modal characterizations of balance are derivable within this system.

cs.LO↗

arXiv2026

Efficient Decision Procedures for RNmatrix Semantics

Logical matrices provide a semantic framework in which connectives are interpreted by deterministic truth-functions. While elegant, this approach is often too restrictive to capture the semantics of many non-classical logics. Non-deterministic matrices (Nmatrices) generalise ordinary matrices by allowing connectives to return a set of possible truth values rather than a unique one, thereby increasing expressive power. Restricted non-deterministic matrices (RNmatrices) further refine this framework by imposing constraints on the rows of Nmatrices, filtering out "unsound" rows and retaining only "valid" ones. This yields a more expressive semantic framework that has been successfully used to provide sound and complete semantics for a wide range of logics, including paraconsistent, intuitionistic, and modal logics. Despite these advances, no efficient decision procedures based on RNmatrix semantics have been proposed. In this paper, we develop automated theorem provers based on RNmatrices by encoding their semantics as Satisfiability Modulo Theories (SMT) problems. The resulting provers decide validity and construct countermodels, achieving state-of-the-art performance for paraconsistent logics and competitive results for intuitionistic and modal logics.

cs.LO↗

arXiv2025

The Modal Cube Revisited: Semantics without Worlds (Technical Report)

We present a non-deterministic semantic framework for all modal logics in the modal cube, extending prior works by Kearns and others. Our approach introduces modular and uniform multi-valued non-deterministic matrices (Nmatrices) for each logic, where necessitation is captured by the systematic use of level valuations. The semantics is grounded in an eight-valued system and provides a sound and complete decision procedure for each modal logic, extending and refining earlier semantics as particular cases. Additionally, we propose a novel model-theoretic perspective that links our framework to relational (Kripke-style) semantics, addressing longstanding conjectures regarding the correspondence between modal axioms and semantic conditions within non-deterministic settings. The result is a philosophically robust and technically modular alternative to standard possible-world semantics.

cs.LO↗

arXiv2025

A Constraint Opinion Model

This paper introduces a generalised opinion model that extends the standard DeGroot model by representing agents' opinions and influences as soft constraints rather than single real values. This allows for modelling scenarios beyond the scope of the DeGroot model, such as agents sharing partial information and preferences, engaging in discussions on multiple topics simultaneously, and representing opinions with different degrees of uncertainty. By considering soft constraints as influences, the proposed model captures also situations where agents impose conditions on how others' opinions are integrated during belief revision. Finally, the flexibility offered by soft constraints allows us to introduce a novel polarisation measure that takes advantage of this generalised framework.

cs.LO↗

arXiv2024

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

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.

cs.LO↗

arXiv2024

Reasoning About Group Polarization: From Semantic Games to Sequent Systems

Group polarization, the phenomenon where individuals become more extreme after interacting, has been gaining attention, especially with the rise of social media shaping people's opinions. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this work we consider the modal logic PNL that captures the notion of agents agreeing or disagreeing on a given topic. Our contribution involves enhancing PNL with advanced formal reasoning techniques, instead of relying on axiomatic systems for analyzing group polarization. To achieve this, we introduce a semantic game tailored for (hybrid) extensions of PNL. This game fosters dynamic reasoning about concrete network models, aligning with our goal of strengthening PNL's effectiveness in studying group polarization. We show how this semantic game leads to a provability game by systemically exploring the truth in all models. This leads to the first cut-free sequent systems for some variants of PNL. Using polarization of formulas, the proposed calculi can be modularly adapted to consider different frame properties of the underlying model.

cs.LO↗

arXiv2024

Multi-modalities and non-commutativity/associativity in functorial linear logic: a case study

Similar to modal connectives, the exponential ! in intuitionistic linear logic (ILL) is not canonical, in the sense that if $i\not= j$ then $!^i F\not\equiv !^j F$. Intuitively, this means that we can mark the exponential with labels taken from a set I organized in a pre-order $\preceq$, obtaining (possibly infinitely-many) exponentials ($!^i$ for $i\in I$). There are, however, two main differences between multi-modalities in normal modal logics and subexponentials in linear logic. i. substructural behaviour. Subexponentials carry the possibility of having different structural behaviors; ii. nature of modalities. Normal modal logics start from the weakest version, assuming only axiom K, then extensions are considered, by adding other axioms. Exponentials in linear logic "take for granted" the behaviors expressed by axioms T and 4. Regarding (i), originally subexponentials could assume only weakening and contraction axioms, but later non-commutative/non-associative systems allowing commutative/ associative subexponentials were presented. Concerning (ii), Guerrini et al unified the modal and LL approaches, with the exponentials assuming only the linear version of K, with the possibility of adding modal extensions to it. This discussion was brought to multi-modal case, where subexponentials consider not only the structural axioms for contraction and weakening, but also the subexponential version of axioms {K,4,D,T}. In this work, we intend to join these two studies. This means that $!^{i}$ can behave classically or not, model associative and commutative systems or not, but also with exponential behaviors different from those in LL. Hence, by assigning different modal axioms one obtains, in a modular way, a class of different substructural modal logics.

cs.LO↗

arXiv2024

Timed Strategies for Real-Time Rewrite Theories

In this paper we propose a language for conveniently defining a wide range of execution strategies for real-time rewrite theories, and provide Maude-strategy-implemented versions of most Real-Time Maude analysis methods, albeit with user-defined discrete and timed strategies. We also identify a new time sampling strategy that should provide both efficient and exhaustive analysis for many distributed real-time systems. We exemplify the use of our language and its analyses on a simple round trip time protocol, and compare the performance of standard Maude search with our strategy-implemented reachability analyses on the CASH scheduling algorithm benchmark.

cs.LO↗

arXiv2024

Unified Opinion Dynamic Modeling as Concurrent Set Relations in Rewriting Logic

Social media platforms have played a key role in weaponizing the polarization of social, political, and democratic processes. This is, mainly, because they are a medium for opinion formation. Opinion dynamic models are a tool for understanding the role of specific social factors on the acceptance/rejection of opinions because they can be used to analyze certain assumptions on human behaviors. This work presents a framework that uses concurrent set relations as the formal basis to specify, simulate, and analyze social interaction systems with dynamic opinion models. Standard models for social learning are obtained as particular instances of the proposed framework. It has been implemented in the Maude system as a fully executable rewrite theory that can be used to better understand how opinions of a system of agents can be shaped. This paper also reports an initial exploration in Maude on the use of reachability analysis, probabilistic simulation, and statistical model checking of important properties related to opinion dynamic models.

cs.LO↗

arXiv2023

Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop brings together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.

cs.LO↗

arXiv2023

Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models

Expressing attack-defence 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 agents' 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.

cs.MA↗

arXiv2023

Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving

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 Roméo 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 Roméo in many cases.

cs.LO↗

arXiv2022

A Rewriting Logic Semantics and Statistical Analysis for Probabilistic Event-B

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.

cs.LO↗

arXiv2022

A Subexponential View of Domains in Session Types

Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different perspectives. In the last decade, the seminal work of Caires and Pfenning showed that formulas in LL can be interpreted as session types and processes in the pi-calculus as proof terms. This leads to a Curry-Howard interpretation where proof reductions in the cut-elimination procedure correspond to process reductions/interactions. The subexponentials in LL have also played an important role in concurrent systems since they can be interpreted in different ways, including timed, spatial and even epistemic modalities in distributed systems. In this paper we address the question: What is the meaning of the subexponentials from the point of view of a session type interpretation? Our answer is a pi-like process calculus where agents reside in locations/sites and they make it explicit how the communication among the different sites should happen. The design of this language relies completely on the proof theory of the subexponentials in LL, thus extending the Caires-Pfenning interpretation in an elegant way.

cs.LO↗

arXiv2021

A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems

This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, 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, and use rewrite- and narrowing-based reasoning -- 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.

cs.LO↗

arXiv2020

A Semantic Framework for PEGs

Parsing Expression Grammars (PEGs) are a recognition-based formalism which allows to describe the syntactical and the lexical elements of a language. The main difference between Context-Free Grammars (CFGs) and PEGs relies on the interpretation of the choice operator: while the CFGs' unordered choice e | e' is interpreted as the union of the languages recognized by e and e, the PEGs' prioritized choice e/e' discards e' if e succeeds. Such subtle, but important difference, changes the language recognized and yields more efficient parsing algorithms. This paper proposes a rewriting logic semantics for PEGs. We start with a rewrite theory giving meaning to the usual constructs in PEGs. Later, we show that cuts, a mechanism for controlling backtracks in PEGs, finds also a natural representation in our framework. We generalize such mechanism, allowing for both local and global cuts with a precise, unified and formal semantics. Hence, our work strives at better understanding and controlling backtracks in parsers for PEGs. The semantics we propose is executable and, besides being a parser with modest efficiency, it can be used as a playground to test different optimization ideas. More importantly, it is a mathematical tool that can be used for different analyses.

cs.FL↗

arXiv2020

Computational Logic for Biomedicine and Neurosciences

We advocate here the use of computational logic for systems biology, as a \emph{unified and safe} framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The potential candidate logics should have a traditional proof theoretic pedigree (including either induction, or a sequent calculus presentation enjoying cut-elimination and focusing), and should come with certified proof tools. Beyond providing a reliable framework, this allows the correct encodings of our biological systems. % For systems biology in general and biomedicine in particular, we have so far, for the modeling part, three candidate logics: all based on linear logic. The studied properties and their proofs are formalized in a very expressive (non linear) inductive logic: the Calculus of Inductive Constructions (CIC). The examples we have considered so far are relatively simple ones; however, all coming with formal semi-automatic proofs in the Coq system, which implements CIC. In neuroscience, we are directly using CIC and Coq, to model neurons and some simple neuronal circuits and prove some of their dynamic properties. % In biomedicine, the study of multi omic pathway interactions, together with clinical and electronic health record data should help in drug discovery and disease diagnosis. Future work includes using more automatic provers. This should enable us to specify and study more realistic examples, and in the long term to provide a system for disease diagnosis and therapy prognosis.

q-bio.QM↗