Carlos Olarte

Jaime Arias, Kyungmin Bae, Carlos Olarte et al.

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.

Jean-Baptiste Joinet, Carlos Olarte

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.

Renato R. Leme, Carlos Olarte, Elaine Pimentel

Restricted non-deterministic matrices (RNmatrices) impose constraints on the rows of non-deterministic matrices (Nmatrices), filtering out ``unsound" rows and retaining only ``valid" ones. This yields a more expressive framework than standard Nmatrices. Although this approach enables sound and complete semantics for a broad class of logics, \eg, paraconsistent logics, propositional intuitionistic logic, and the fifteen normal modal logics of the modal cube, no {\em efficient} decision procedures based on these semantics have been proposed. In this paper, we implement the RNmatrix framework to develop a new suite of automated theorem provers for these logics. By encoding RNmatrices and their elimination criteria as Satisfiability Modulo Theories (SMT) problems, we leverage SMT solvers to decide formula validity and construct countermodels. We illustrate the method for paraconsistent logics, where our prover outperforms the current state-of-the-art and provides the first implementation for the entire $C_n$ hierarchy, as well as for intuitionistic and modal logics, where our general-purpose prover achieves competitive performance.