International audience

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.

We introduce a DeGroot-based model for opinion dynamics in social networks. A community of agents is represented as a weighted directed graph whose edges indicate how much agents influence one another. The model is formalized using labeled transition systems, henceforth called opinion transition systems (OTS), whose states represent the agents' opinions and whose actions are the edges of the influence graph. If a transition labeled (i,j) is performed, agent j updates their opinion taking into account the opinion of agent i and the influence i has over j. We study (convergence to) opinion consensus among the agents of strongly-connected graphs with influence values in the interval (0,1). We show that consensus cannot be guaranteed under the standard strong fairness assumption on transition systems. We derive that consensus is guaranteed under a stronger notion from the literature of concurrent systems; bounded fairness. We argue that bounded-fairness is too strong of a notion for consensus as it almost surely rules out random runs and it is not a constructive liveness property. We introduce a weaker fairness notion, called m-bounded fairness, and show that it guarantees consensus. The new notion includes almost surely all random runs and it is a constructive liveness property. Finally, we consider OTS with dynamic influence and show convergence to consensus holds under m-bounded fairness if the influence changes within a fixed interval [L,U] with 0 < L < U < 1. We illustrate OTS with examples and simulations, offering insights into opinion formation under fairness and dynamic influence.

We describe a model for polarization in multi-agent systems based on Esteban and Ray's standard family of polarization measures from economics. Agents evolve by updating their beliefs (opinions) based on an underlying influence graph, as in the standard DeGroot model for social learning, but under a confirmation bias; i.e., a discounting of opinions of agents with dissimilar views. We show that even under this bias polarization eventually vanishes (converges to zero) if the influence graph is strongly-connected. If the influence graph is a regular symmetric circulation, we determine the unique belief value to which all agents converge. Our more insightful result establishes that, under some natural assumptions, if polarization does not eventually vanish then either there is a disconnected subgroup of agents, or some agent influences others more than she is influenced. We also prove that polarization does not necessarily vanish in weakly-connected graphs under confirmation bias. Furthermore, we show how our model relates to the classic DeGroot model for social learning. We illustrate our model with several simulations of a running example about polarization over vaccines and of other case studies. The theoretical results and simulations will provide insight into the phenomenon of polarization.

One of the main concerns about fairness in machine learning (ML) is that, in order to achieve it, one may have to trade off some accuracy. To overcome this issue, Hardt et al. proposed the notion of equality of opportunity (EO), which is compatible with maximal accuracy when the target label is deterministic with respect to the input features. In the probabilistic case, however, the issue is more complicated: It has been shown that under differential privacy constraints, there are data sources for which EO can only be achieved at the total detriment of accuracy, in the sense that a classifier that satisfies EO cannot be more accurate than a trivial (random guessing) classifier. In our paper we strengthen this result by removing the privacy constraint. Namely, we show that for certain data sources, the most accurate classifier that satisfies EO is a trivial classifier. Furthermore, we study the trade-off between accuracy and EO loss (opportunity difference), and provide a sufficient condition on the data source under which EO and non-trivial accuracy are compatible.

Spatial constraint systems (scs) are semantic structures for reasoning about spatial and epistemic information in concurrent systems. We develop the theory of scs to reason about the distributed information of potentially infinite groups. We characterize the notion of distributed information of a group of agents as the infimum of the set of join-preserving functions that represent the spaces of the agents in the group. We provide an alternative characterization of this notion as the greatest family of join-preserving functions that satisfy certain basic properties. We show compositionality results for these characterizations and conditions under which information that can be obtained by an infinite group can also be obtained by a finite group. Finally, we provide algorithms that compute the distributive group information of finite groups.

This issue of Mathematical Structures in Computer Science (MSCS) contains a selection of papers presented at the 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), which took place in Cali, Colombia, on October 29–31, 2015.

This issue of Mathematical Structures in Computer Science contains a selection of papers presented at the 17th International Workshop on Expressiveness in Concurrency (EXPRESS'10), a satellite event of CONCUR'10, held on August 30th in Paris, France.

This issue of Mathematical Structures in Computer Science contains a selection of papers presented at the 18th International Workshop on Expressiveness in Concurrency (EXPRESS'11), a satellite event of CONCUR'11, held on September 5th, 2011 in Aachen, Germany.

We enrich spatial constraint systems with operators to specify information and processes moving from a space to another. We shall refer to these news structures as spatial constraint systems with extrusion. We shall investigate the properties of this new family of constraint systems and illustrate their applications. From a computational point of view the new operators provide for process/information extrusion, a central concept in formalisms for mobile communication. From an epistemic point of view extrusion corresponds to a notion we shall call utterance; a piece of information that an agent communicates to others but that may be inconsistent with the agent's beliefs. Utterances can then be used to express instances of epistemic notions, which are common place in social media, such as hoaxes or intentional lies. Spatial constraint systems with extrusion can be seen as complete Heyting algebras equipped with maps to account for spatial and epistemic specifications.

Concurrent Constraint Programming (ccp) is a well-established declarative framework from concurrency theory. Its foundations and principles e.g., semantics, proof systems, axiomatizations, have been thoroughly studied for over the last two decades. In contrast, the development of algorithms and automatic verification procedures for ccp have hitherto been far too little considered. To the best of our knowledge there is only one existing verification algorithm for the standard notion of ccp program (observational) equivalence. In this paper we first show that this verification algorithm has an exponential-time complexity even for programs from a representative sub-language of ccp; the summation-free fragment (ccp\+). We then significantly improve on the complexity of this algorithm by providing two alternative polynomial-time decision procedures for ccp\+ program equivalence. Each of these two procedures has an advantage over the other. One has a better time complexity. The other can be easily adapted for the full language of ccp to produce significant state space reductions. The relevance of both procedures derives from the importance of ccp\+. This fragment, which has been the subject of many theoretical studies, has strong ties to first-order logic and an elegant denotational semantics, and it can be used to model real-world situations. Its most distinctive feature is that of confluence, a property we exploit to obtain our polynomial procedures.

The timed concurrent constraint programing model (tcc) is a declarative framework, closely related to First-Order Linear Temporal Logic (FLTL), for modeling reactive systems. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols.

We present an expressiveness study of linearity and persistence of processes. We choose the ð-calculus, one of the main representatives of process calculi, as a framework to conduct our study. We consider four fragments of the ð-calculus. Each one singles out a natural source of linearity/ persistence also present in other frameworks such as Concurrent Constraint Programming (CCP), Linear CCP, and several calculi for security. The study is presented by providing (or proving the non-existence of) encodings among the fragments, a processes-as-formulae interpretation and a reduction from Minsky machines.

The tcc paradigm is a formalism for timed concurrent constraint programming. Several tcc languages differing in their way of expressing infinite behavior have been proposed in the literature. In this paper we study the expressive power of some of these languages. In particular, we show that: (1) recursive procedures with parameters can be encoded into parameterless recursive procedures with dynamic scoping, and viceversa. (2) replication can be encoded into parameterless recursive procedures with static scoping, and viceversa. (3) the languages from (1) are strictly more expressive than the languages from (2). Furthermore, we show that behavioral equivalence is undecidable for the languages from (1), but decidable for the languages from (2). The undecidability result holds even if the process variables take values from a fixed finite domain.