Processes of opinion formation rooted in social dynamics can significantly contribute to the polarization of social, political, and democratic interaction. Opinion dynamic models are essential for understanding the impact of specific social factors on the acceptance or rejection of opinions. This extended paper builds upon the conference presentation documented in [1] , introducing improvements and new opinion models that explore biases and collective human behaviors. It presents a framework based on concurrent set relations that formalizes, simulates, and analyzes social interaction systems with dynamic opinion models. Within this framework, standard models for social learning are realized as specific instances. Implemented in the Maude system as a fully executable rewrite theory, the framework enables a detailed examination of how agents' opinions can be influenced within a system. The authors report on new formalization of several and existing social learning models, exploring their relationships with different concurrency models. New experimentation involving reachability analysis, probabilistic simulation, and statistical model checking has been conducted. These experiments are crucial for validating significant properties related to dynamic opinion models in Maude, offering new insights into the mechanisms of opinion shaping in social interaction.

P is a domain-specific language designed for specifying asynchronous, event-driven systems. Its computational model is based on actors, i.e., on communicating state machines. This paper presents a formal semantics of P using rewriting logic, extending the language's verification capabilities. Implemented in Maude, a rewriting logic language, this semantics enables automated analysis of P programs, including reachability analysis, LTL model checking, and statistical model checking. Through illustrative examples, this paper demonstrates how this formalization significantly enhances P 's verification capacities in practical scenarios.

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.

BACKGROUND: 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. CONCLUSIONS: 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.

A blockchain is a distributed hierarchical data structure. Widely-used applications of blockchain include digital currencies such as Bitcoin and Ethereum. This paper proposes an algorithmic approach to analyze the efficiency of a blockchain as a function of the number of blocks and the average synchronization delay. The proposed algorithms consider a random network model that characterizes the growth of a tree of blocks by adhering to a standard protocol. The model is parametric on two probability distribution functions governing block production and communication delay. Both distributions determine the synchronization efficiency of the distributed copies of the blockchain among the so- called workers and, therefore, are key for capturing the overall stochastic growth. Moreover, the algorithms consider scenarios with a fixed or an unbounded number of workers in the network. The main result illustrates how the algorithms can be used to evaluate different types of blockchain designs, e.g., systems in which the average time of block production can match the average time of message broadcasting required for synchronization. In particular, this algorithmic approach provides insight into efficiency criteria for identifying conditions under which increasing block production has a negative impact on the stability of a blockchain. The model and algorithms are agnostic of the blockchain’s final use, and they serve as a formal framework for specifying and analyzing a variety of non-functional properties of current and future blockchains.

The Integrated and Configurable Algorithms for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture being developed for the robust integration of mission-specific software modules and highly assured core software modules. This paper reports on the use of automatic reachability analysis during the development of ICAROUS, as a first step towards a broader formal verification effort of the software architecture. It explains how simulation based on state-space exploration and LTL model checking has been performed on a formal executable specification of the system in rewriting logic. Overall, this effort has unveiled issues such as deadlocks and undesired behavior, and has helped improve the ICAROUS design and source code.