arXiv subjects

Camilo Rocha

Publications and source records attributed to Camilo Rocha.

16 recordsLinked to original sources

arXiv2026

Equational and Inductive Reasoning for Maude in Athena

In the rewriting logic framework, equational-based specifications are used to define deterministic functional behavior, abstract data types, and canonical representations of data. These specifications include a (possibly order-sorted) signature and equations interpreted modulo structural axioms, such as associativity, commutativity, and identity. While equational rewriting provides a powerful basis for execution and symbolic reasoning, it does not by itself offer native support for inductive or deductive reasoning. This paper presents maude2athena, a framework that systematically translates Maude's equational theories into Athena, a theorem proving language designed to support natural deduction proofs over many-sorted first-order logic specifications, including inductive reasoning, equational chaining, case-based reasoning, and proofs by contradiction. The translation supports induction-based reasoning modulo structural axioms with parametric induction rules; it faithfully encodes membership equational logic in a many-sorted setting without exponential blowup under reasonable conditions. This approach preserves the semantics of the original specification, while ensuring that the translation remains compact and amenable to deductive reasoning. This work helps bridge the gap between model checking and theorem proving, enabling formal verification efforts that can benefit from both of these approaches.

cs.LO↗

arXiv2024

Consensus in Models for Opinion Dynamics with Generalized-Bias

Interest is growing in social learning models where users share opinions and adjust their beliefs in response to others. This paper introduces generalized-bias opinion models, an extension of the DeGroot model, that captures a broader range of cognitive biases. These models can capture, among others, dynamic (changing) influences as well as ingroup favoritism and out-group hostility, a bias where agents may react differently to opinions from members of their own group compared to those from outside. The reactions are formalized as arbitrary functions that depend, not only on opinion difference, but also on the particular opinions of the individuals interacting. Under certain reasonable conditions, all agents (despite their biases) will converge to a consensus if the influence graph is strongly connected, as in the original DeGroot model. The proposed approach combines different biases, providing deeper insights into the mechanics of opinion dynamics and influence within social networks.

cs.SI↗

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↗

arXiv2022

A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and Verification

This paper addresses the issue of specifying, simulating, and verifying reactive systems in rewriting logic. It presents an executable semantics for probabilistic, timed, and spatial concurrent constraint programming -- here called stochastic and spatial concurrent constraint systems (SSCC) -- in the rewriting logic semantic framework. The approach is based on an enhanced and generalized model of concurrent constraint programming (CCP) where computational hierarchical spaces can be assigned to belong to agents. The executable semantics faithfully represents and operationally captures the highly concurrent nature, uncertain behavior, and spatial and epistemic characteristics of reactive systems with flow of information. In SSCC, timing attributes -- represented by stochastic duration -- can be associated to processes, and exclusive and independent probabilistic choice is also supported. SMT solving technology, available from the Maude system, is used to realize the underlying constraint system of SSCC with quantifier-free formulas over integers and reals. This results in a fully executable real-time symbolic specification that can be used for quantitative analysis in the form of statistical model checking. The main features and capabilities of SSCC are illustrated with examples throughout the paper. This contribution is part of a larger research effort aimed at making available formal analysis techniques and tools, mathematically founded on the CCP approach, to the research community.

cs.LO↗

arXiv2022

Hierarchy exploitation to detect missing annotations on hierarchical multi-label classification

The availability of genomic data has grown exponentially in the last decade, mainly due to the development of new sequencing technologies. Based on the interactions between genes (and gene products) extracted from the increasing genomic data, numerous studies have focused on the identification of associations between genes and functions. While these studies have shown great promise, the problem of annotating genes with functions remains an open challenge. In this work, we present a method to detect missing annotations in hierarchical multi-label classification datasets. We propose a method that exploits the class hierarchy by computing aggregated probabilities to the paths of classes from the leaves to the root for each instance. The proposed method is presented in the context of predicting missing gene function annotations, where these aggregated probabilities are further used to select a set of annotations to be verified through in vivo experiments. The experiments on Oriza sativa Japonica, a variety of rice, showcase that incorporating the hierarchy of classes into the method often improves the predictive performance and our proposed method yields superior results when compared to competitor methods from the literature.

cs.LG↗

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

Feature extraction using Spectral Clustering for Gene Function Prediction using Hierarchical Multi-label Classification

Gene annotation addresses the problem of predicting unknown associations between gene and functions (e.g., biological processes) of a specific organism. Despite recent advances, the cost and time demanded by annotation procedures that rely largely on in vivo biological experiments remain prohibitively high. This paper presents a novel in silico approach for to the annotation problem that combines cluster analysis and hierarchical multi-label classification (HMC). The approach uses spectral clustering to extract new features from the gene co-expression network (GCN) and enrich the prediction task. HMC is used to build multiple estimators that consider the hierarchical structure of gene functions. The proposed approach is applied to a case study on Zea mays, one of the most dominant and productive crops in the world. The results illustrate how in silico approaches are key to reduce the time and costs of gene annotation. More specifically, they highlight the importance of: (i) building new features that represent the structure of gene relationships in GCNs to annotate genes; and (ii) taking into account the structure of biological processes to obtain consistent predictions.

cs.LG↗

arXiv2022

Identifying Stress Responsive Genes using Overlapping Communities in Co-expression Networks

This paper proposes a workflow to identify genes that respond to specific treatments in plants. The workflow takes as input the RNA sequencing read counts and phenotypical data of different genotypes, measured under control and treatment conditions. It outputs a reduced group of genes marked as relevant for treatment response. Technically, the proposed approach is both a generalization and an extension of WGCNA. It aims to identify specific modules of overlapping communities underlying the co-expression network of genes. Module detection is achieved by using Hierarchical Link Clustering. The overlapping nature of the systems' regulatory domains that generate co-expression can be identified by such modules. LASSO regression is employed to analyze phenotypic responses of modules to treatment. Results. The workflow is applied to rice (Oryza sativa), a major food source known to be highly sensitive to salt stress. The workflow identifies 19 rice genes that seem relevant in the response to salt stress. They are distributed across 6 modules: 3 modules, each grouping together 3 genes, are associated to shoot K content; 2 modules of 3 genes are associated to shoot biomass; and 1 module of 4 genes is associated to root biomass. These genes represent target genes for the improvement of salinity tolerance in rice. Conclusion. A more effective framework to reduce the search-space for target genes that respond to a specific treatment is introduced. It facilitates experimental validation by restraining efforts to a smaller subset of genes of high potential relevance.

q-bio.MN↗

arXiv2022

A Top-down Supervised Learning Approach to Hierarchical Multi-label Classification in Networks

Node classification is the task of inferring or predicting missing node attributes from information available for other nodes in a network. This paper presents a general prediction model to hierarchical multi-label classification (HMC), where the attributes to be inferred can be specified as a strict poset. It is based on a top-down classification approach that addresses hierarchical multi-label classification with supervised learning by building a local classifier per class. The proposed model is showcased with a case study on the prediction of gene functions for Oryza sativa Japonica, a variety of rice. It is compared to the Hierarchical Binomial-Neighborhood, a probabilistic model, by evaluating both approaches in terms of prediction performance and computational cost. The results in this work support the working hypothesis that the proposed model can achieve good levels of prediction efficiency, while scaling up in relation to the state of the art.

cs.LG↗

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

Spectral Evolution with Approximated Eigenvalue Trajectories for Link Prediction

The spectral evolution model aims to characterize the growth of large networks (i.e., how they evolve as new edges are established) in terms of the eigenvalue decomposition of the adjacency matrices. It assumes that, while eigenvectors remain constant, eigenvalues evolve in a predictable manner over time. This paper extends the original formulation of the model twofold. First, it presents a method to compute an approximation of the spectral evolution of eigenvalues based on the Rayleigh quotient. Second, it proposes an algorithm to estimate the evolution of eigenvalues by extrapolating only a fraction of their approximated values. The proposed model is used to characterize mention networks of users who posted tweets that include the most popular political hashtags in Colombia from August 2017 to August 2018 (the period which concludes the disarmament of the Revolutionary Armed Forces of Colombia). To evaluate the extent to which the spectral evolution model resembles these networks, link prediction methods based on learning algorithms (i.e., extrapolation and regression) and graph kernels are implemented. Experimental results show that the learning algorithms deployed on the approximated trajectories outperform the usual kernel and extrapolation methods at predicting the formation of new edges.

cs.LG↗

arXiv2020

Verification of the IBOS Browser Security Properties in Reachability Logic

This paper presents a rewriting logic specification of the Illinois Browser Operating System (IBOS) and defines several security properties, including the same-origin policy (SOP) in reachability logic. It shows how these properties can be deductively verified using our constructor-based reachability logic theorem prover. This paper also highlights the reasoning techniques used in the proof and three modularity principles that have been crucial to scale up and complete the verification effort.

cs.LO↗

arXiv2019

A Random Network Model for the Analysis of Blockchain Designs with Communication Delay

This paper proposes a random network model for blockchains, a distributed hierarchical data structure of blocks that has found several applications in various industries. The model is parametric on two probability distribution functions governing block production and communication delay, which are key to capture the complexity of the mechanism used to synchronize the many distributed local copies of a blockchain. The proposed model is equipped with simulation algorithms for both bounded and unbounded number of distributed copies of the blockchain. They are used to study fast blockchain systems, i.e., blockchains in which the average time of block production can match the average time of message broadcasting used for blockchain synchronization. In particular, the model and the algorithms are useful to understand efficiency criteria associated with fast blockchains for identifying, e.g., when increasing the block production will have negative impact on the stability of the distributed data structure given the network's broadcast delay.

cs.DC↗

arXiv2019

Estimating Formation Mechanisms and Degree Distributions in Mixed Attachment Networks

Our work introduces an approach for estimating the contribution of attachment mechanisms to the formation of growing networks. We present a generic model in which growth is driven by the continuous attachment of new nodes according to random and preferential linkage with a fixed probability. Past approaches apply likelihood analysis to estimate the probability of occurrence of each mechanism at a particular network instance, exploiting the concavity of the likelihood function at each point in time. However, the probability of connecting to existing nodes, and consequently the likelihood function itself, varies as networks grow. We establish conditions under which applying likelihood analysis guarantees the existence of a local maximum of the time-varying likelihood function and prove that an expectation maximization algorithm provides a convergent estimate. Furthermore, the in-degree distributions of the nodes in the growing networks are analytically characterized. Simulations show that, under the proposed conditions, expectation maximization and maximum-likelihood accurately estimate the actual contribution of each mechanism, and in-degree distributions converge to stationary distributions.

math.PR↗

arXiv2018

Reachability Analysis for Spatial Concurrent Constraint Systems with Extrusion

Spatial concurrent constraint programming (SCCP) is an algebraic model of spatial modalities in constrained-based process calculi; it can be used to reason about spatial information distributed among the agents of a system. This work presents an executable rewriting logic semantics of SCCP with extrusion (i.e., process mobility) that uses rewriting modulo SMT, a novel technique that combines the power of term rewriting, matching algorithms, and SMT-solving. In this setting, constraints are encoded as formulas in a theory with a satisfaction relation decided by an SMT solver, while the topology of the spatial hierarchy is encoded as part of the term structure of symbolic states. By being executable, the rewriting logic specification offers support for the inherent symbolic and challenging task of reachability analysis in the constrained-based model. The approach is illustrated with examples about the automatic verification of fault-tolerance, consistency, and privacy in distributed spatial and hierarchical systems.

cs.LO↗

arXiv2010

Rewriting Logic Semantics of a Plan Execution Language

The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXIL executives. The implementation in Maude has the additional benefit of making available to PLEXIL designers and developers all the formal analysis and verification tools provided by Maude. The formalization of the PLEXIL semantics in rewriting logic poses an interesting challenge due to the synchronous nature of the language and the prioritized rules defining its semantics. To overcome this difficulty, we propose a general procedure for simulating synchronous set relations in rewriting logic that is sound and, for deterministic relations, complete. We also report on two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude.

cs.PL↗