Michelangelo Fiore
email: ⋆mfiore@laas.fr

Aurélie Clodic 1⋆⋆ Rachid Alami
email: rachid.alami@laas.fr

On Planning and Task achievement Modalities for Human-Robot Collaboration

Keywords: Human-Robot Interaction, Control Architectures, Robot Supervision

In this paper we present a robot supervision system designed to be able to execute collaborative tasks with humans in a flexible and robust way. Our system is designed to take into account the different preferences of the human partners, providing three operation modalities to interact with them. The robot is able to assume a leader role, planning and monitoring the execution of the task for itself and the human, to act as assistent of the human partner, following his orders, and also to adapt its plans to the human actions. We present several experiments that show that the robot can execute collaborative tasks with humans.

Introduction

In Human-Robot Interaction robots must be equipped with a complex set of skills, which allows them to reason about human agents intentions and statuses and to act accordingly. When interacting with a robot, different users will have different preferences. The robot must be able to take into account these preferences and provide different operation modalities to allow more natural interaction with the human. We have designed a system able to cooperate with humans to complete joint goals.

We present an object manipulation scenario, composed by tasks, such as fetching, giving objects and other collaborative operations, which are typical of domestic environments. In this scenario a human and a robot must cooperate to complete a joint goal, which is a kind of goal that requires both agents to work together. This joint goal is known by both partners at the start of the scenario, perhaps because it has being agreed in a first interaction process. We have identified several ways -or modalities -to envisage how the robot planning and decisional abilities for task achievement can be used:

-Human Plans. The robot is not aware of the global plan or does not reason about the long-term global goal. The human decides when to ask the robot to perform individual tasks. The robot then acts by performing, in the context, the requested task. Decisional autonomy here is limited to how the robot refines and performs the task in the context. The robot is not completely passive when not executing an operation since it will continuously monitor and update the state of the environment. -Robot plans. There is a joint goal between the human and the robot. The robot builds the 'best' plan to achieve this goal, taking into account the world status, the abilities of the two agents and the preferences of the human, then it verbalizes it and achieves it by doing its 'part of the job' and monitoring the human activity. This modality corresponds to a fully agreed upon plan that is built on-line or even predefined and known to both agents. -Robot adapts. There is a joint goal between the human and the robot. The robot monitors what the human is doing and whenever possible, tries to achieve an action or a set of actions that advances the plan toward the goal. This could be seen as an intelligent robot reaction to the context including the possibility to have the robot proactively facilitating the action of the human whenever possible.

We think that the interaction process should be flexible, allowing eventually the robot to switch modality depending on the task status and of the human actions or simply upon request. To be able to interact with a human agent in a natural way, the robot needs to possess a number of different mechanisms, such as joint attention, action observation, task-sharing and action coordination. Using these mechanisms the robot can create shared plans, that take into account the capacities of both agents, and execute them in a coordinated way. We have developed an architecture and decisional components which allow us to run these different interaction modalities. The goal of the paper is not to provide a detailed description of any of these components but rather to provide a global view of the system and to show its flexibility.

Related Work

The topic of joint actions has been studied by different authors in the field of psychology. In [START_REF] Bratman | Shared agency. Philosophy of the social sciences: philosophical theory and scientific practice[END_REF] Bratman proposes a definition of the topic, giving several conditions deemed necessary to perform a joint action. Other researchers [START_REF] Mutlu | Coordination mechanisms in human-robot collaboration[END_REF] [START_REF] Sebanz | Joint action: bodies and minds moving together[END_REF] have studied a number of key mechanisms necessary to support joint actions between different partners: joint attention, action observation, task-sharing, action coordination and perception of agency.

Individual engaging in joint action use several ways, like language, gaze cues and gestures to establish a common ground. This mechanism appears to be crucial in successfully performing joint actions. Perspective taking, which is studied in psychology literature [START_REF] Flavell | Perspectives on Perspective Taking[END_REF][START_REF] Tversky | Why do speakers mix perspectives?[END_REF], is a critical mechanism when interacting with people by allowing one to reason on others' understanding of the world in terms of visual perception, spatial descriptions, affordances and beliefs, etc. In [START_REF] Ros | Which One? Grounding the Referent Based on Efficient Human-Robot Interaction[END_REF] perspective taking is used to solve ambiguities in a human-robot interaction scenario by reasoning from the partner's point of view. In [START_REF] Trafton | Enabling Effective Human-robot Interaction Using Perspective-taking in Robots[END_REF] perspective taking is integrated in a robotic system and applied to several kinds of problems.

Spatial reasoning [START_REF] O'keefe | The Spatial Prepositions[END_REF], has been used for natural language processing for applications such as direction recognition [START_REF] Kollar | Toward understanding natural language directions[END_REF][START_REF] Matuszek | Following Directions Using Statistical Machine Translation[END_REF] or knowledge grounding [START_REF] Lemaignan | Anchoring interaction through symbolic knowledge[END_REF]. [START_REF] Skubic | Spatial language for human-robot dialogs[END_REF] presented a spatial reasoner integrated in a robot which computes symbolic positions of objects.

Understanding what other agents are doing is necessary to perform a joint action. In [START_REF] Gray | Action parsing and goal inference using self as simulator[END_REF] the authors allow a robot to monitor users' actions by simulating their behaviors with the robot's motor, goal and perceptual levels. In [START_REF] Demiris | Hierarchical attentive multiple models for execution and recognition of actions[END_REF] the authors present the HAMMER architecture, based on the idea of using inverse and forward models arranged in hierarchical and parallel manners. With this architecture the authors are able to use the same model to execute and recognize actions, an idea compatible with several biological evidences.

Other agents' actions can be predicted in different ways. By observing another agents we can predict the outcomes of their actions and understand what they're going to do next. Participants in a joint action form a shared representation of a task, used to predict other partners' actions. In [START_REF] Karami | Human-robot collaboration for a shared mission[END_REF] human intentions are estimated using a POMDP (Partially Observable Markov Decision Process) and a set of MDP (Markov Decision Process), that simulate human policies related to different intentions. However, predicting other agents' action is not enough to participate in a joint action, because the agent needs also to choose appropriate complementary actions, adapting them to the capability of the participants. The agents need to create a coordinated plan, giving particular care to timing information. In [START_REF] Nikolaidis | Human-robot cross-training: computational formulation, modeling and evaluation of a human team training strategy[END_REF] the idea of cross-training is applied to shared-planning. A human and a robot iteratively switch roles to learn a shared plan for a collaborative task. This strategy is compared to standard reinforcement learning techniques, showing improvements in performances. These results support the idea of modeling practices for human teamwork in human robot interaction. In [START_REF] Shah | Improved humanrobot team performance using chaski, a human-inspired plan execution system[END_REF] a shared plan is executed using Chaski, a task-level executive which is used to adapt the robot's actions to the human partners. Plans can be executed in two different modalities: equal partners or leader and assistant. The authors show that this system reduces human idle time. In [START_REF] Hema | Anticipating human activities using object affordances for reactive robotic response[END_REF] an anticipatory temporal conditional random field is used to estimate possible users' actions, based on the calculation of object affordances and possible user trajectories. With this knowledge the robot can anticipate users' actions and react accordingly. In [START_REF] Cirillo | A Framework For Human-Aware Robot Planning[END_REF] the authors present a framework for human aware planning where the robot can observe and estimate human plans to coordinate its activites with those of the human partners. The framework doesn't support direct human-robot interaction.

Communication between partners in a joint task is crucial. The robot needs to be able to give information to its partners in a clear and socially acceptable way. [START_REF] Torrey | How a robot should give advice[END_REF] proposes different strategies to modulate robot speech in order to produce more socially acceptable messages. In [START_REF] Liu | It's not polite to point: generating socially-appropriate deictic behaviors towards people[END_REF] the authors study how to generate socially appropriate deictic behaviors in a robot, balancing understandability and social appropriateness.

Few robotic architectures take humans into account to allow the execution of human-robot joint actions. [START_REF] Trafton | ACT-R/E: An Embodied Cognitive Architecture for Human-Robot Interaction[END_REF] presents ACT-R/E, a cognitive architecture, based on the ACT-R architecture, used for human robot interaction tasks. The architecture aims at simulating how humans think, perceive and act in the world. ACT-R/E has being tested in different scenarios, such as theory of mind and hide and seek, to show its capacity of modeling human behaviors and tought. In [START_REF] Fong | The Human-Robot Interaction Operating System[END_REF] the authors present HRI/OS, an agent-based system that allows humans and robots to work in teams. The system is able to produce and schedule tasks to different agents, based on their capacities, and allows the agents to interact mostly in a parallel and independent way, with loose coordination between them. Cooperation mainly takes place when one agent asks for help while dealing with a situation. In this case the HRI/OS will look for the best agent to help, based on their availability and capacities. In [START_REF] Clodic | Shary: a supervision system adapted to human-robot interaction[END_REF] the authors build SHARY, a supervision system for human robot interaction, tested in domestic environments to perform tasks such as serving a drink to a person. Our system is an evolution of Shary which includes new aspects, like spatial reasoning and modeling of joint actions.

Technical Approach

Our robot is controlled by an architecture composed of different components as shown in figure 1. Supervision System. The component in charge of commanding the other components of the system in order to complete a task. After receiving a goal the supervision system will use the various planners of the system to obtain a list of actions for the robot and for the human. It will then be in charge of executing the robot actions and to monitor the human part of the plan. Specific treatment is reserved to joint actions (see Collaboration Planners). The supervision system aims at being flexible enough to be used in different robotic systems and robust so that it can recover from plan failures and adapt to human behaviors that are not expected, according to the current plan. HATP. The Human-Aware Task Planner [START_REF] Lallement | HATP: An HTN Planner for Robotics[END_REF], based on a Hierarchical Task Network (HTN) refinement which performs an iterative task de-composition into sub-tasks until reaching atomic actions [START_REF] Nau | SHOP2: An HTN Planning System[END_REF]. HATP is able to produce plans for the robot as well as for the other participants (humans or robots). By setting a different range of parameters the plans can be tuned to adapt the robot behavior to the desired level of cooperation. HATP is able to take into account the different beliefs of each agents when producing a plan, eventually including actions that help creating joint attention [START_REF] Warnier | When the robot puts itself in your shoes. managing and exploiting human and robot beliefs[END_REF]. Collaboration Planners. This set of planners are based on POMDP models used in joint actions, such as handovers, to estimate the user intentions and select an action to perform. In order to mantain a simple and flexible domain, the POMDP selects high level actions (like continue plan or wait for the user), which are adapted by the supervision system to the current situation. We can picture Fig. 1: System Architecture the interaction between HATP, the collaborative planners and the supervision system in the following way. HATP creates a plan composed by different actions to achieve a goal. The supervision system refines and executes each action in the plan, using the collaborative planners to adapt its actions to those of the other agents during a joint action. SPARK. The Spatial Reasoning and Knowledge component, responsible for geometric information gathering [START_REF] Milliez | A framework for endowing interactive robot with reasoning capabilities about perspectivetaking and belief management[END_REF]. SPARK embeds a number of decisional activities linked to abstraction (symbolic facts production) and inference based on geometric and temporal reasoning. SPARK maintains all geometric positions and configurations of agents, objects and furniture coming from perception and previous or a priori knowledge. SPARK computes perspective taking, allowing the system to reason on other agents' beliefs and capacities. Knowledge Base. The facts produced by SPARK are stored in a central symbolic knowledge base. This base mantains a different model for each agent, allowing to represent divergent beliefs. For example, the fact representing the position of an object could point to a different location in two agent models in our knowledge base, representing the different information that the two agents possess. A set of Human aware motion, placement and manipulation planners. These planners are in charge of choosing trajectories for the robot, taking into account the environment and the present agents [START_REF] Sisbot | Supervision and Motion Planning for a Mobile Manipulator Interacting with Humans[END_REF][START_REF] Mainprice | Planning human-aware motions using a sampling-based costmap planner[END_REF][START_REF] Pandey | Mightability maps: A perceptual level decisional framework for co-operative and competitive human-robot interaction[END_REF].

Results

By using the capacities of its different components, our system is able to produce several results in human-robot interaction.

1. Situation Assesment and Planning. Using SPARK and its sensors, the robot is able to create different representations of the world for itself and for the other agents, which are then stored in the Knowledge Base. In this way the robot can take into account what it and the other agents can see, reach and know when creating plans. Using HATP the robot can create a plan constituted by different execution streams for every present agent. As said before, there are three operation modalities in the system: robot plans, user plans and robot adapts.

Robot plans. In the first modality the robot will, using information present in the Knowledge Base and HATP, produce a plan to complete the joint goal.

After that the robot will verbalize the plan to the user, explaining which actions will be performed by each agent and in which order. The robot will monitor the execution process, informing the human of which actions it's about to execute and also on when the human should execute its part of the plan. This modality, where the robot is the leader, can be helpful when interacting with naive users or in tasks where the robot has a better knowledge of the domain or of the environment than the other agents.

Human plans. The human can also create plans, interacting with the robot by using a tablet application. This application allows the user to select different actions and parameters. The user can issue both high level goals (e.g. clean the table) and simpler actions (e.g. take the grey tape, give me the walle tape, stop your current action). The robot will simply observe the surroundings and wait for user inputs. This modality is always available and has a priority over the other two modalities. If the robot receives a command from the application while it is in another modality, it will abandon its current plan, stopping its actions at a safe point, and then execute the users' command. We feel that this interaction modality is important for two different reasons. First, some users will simply prefer to be in charge of the execution process, for a matter of personal preference or because they feel they have a deeper knowledge on how to realize the current task than the robot. We can picture, for example, industrial or medical scenarios, where the human is the leader and asks the robot to perform different tasks to help him, when needed. A second use of this modality is in situations where the robot doesn't have a clear estimation of the users' intentions and goals. For example, in a domestic environment, a user could decide to order a robot to bring him a drink, a need that the robot can't always anticipate. Robot adapts. In the last presented operation modality the robot will try to help the human to complete a task. At the start of the scenario, the robot will stand still and observe the environment. After the user takes an action the robot will calculate a plan and try to help as it can, by performing actions related to that task and by giving helpful information to the user. In our implementation the robot will start this modality in a 'passive' role, simply observing the human until he takes the first action. We could also picture a more pro-active role for the robot, where the robot chooses a goal on its own and starts acting toward its completion, eventually asking for the help of the human when he can't complete an action. This modality corresponds to what we feel is a very natural way of interaction between different partners, in particular in non-critical tasks, where defining an accurate plan between the partners is not fundamental. This situation relates quite easily to the scenario we will present in details in section 5, where the two partners must clean a set of furnitures together. In this situation the two partners could simply choose to start executing the actions that they prefer, continuously adapting their plans to the other partners' actions.

The robot is able to switch from one modality to another during execution. For example, if the robot is in the 'robot plans' modality and the users' actions differ from the calculated plan the robot will interrupt its current action, create a new plan, and switch to the 'robot adapts' modality.

Human Intention Estimation and Reactive Action Execution. Using

the Collaboration Planners we can execute joint actions in a reactive way. For example, in the case of an handover, a POMDP receives as input a set of observations, representing the distance between the human and the robot, the posture of the human arm and the user's orientation, used to estimate the current user intentions (i.e. user engaged, not engaged, not interested in the task). Using this information and the other variables that model the task status, the POMDP selects high level actions that are adapted by the supervisor. For example, the POMDP could decide to wait for an user that is not currently engaged in the joint action, but hasn't abandoned the task yet. The supervision system at this point will decide in which posture and for how long to wait for the user. If the user shows again interest in the task, the POMDP could select a 'continue plan' action, and the supervision system could choose to extend the robot arm as response. 3. Human Action Monitor. Using SPARK, the system is able to monitor human actions by creating Monitor Spheres associated to items considered interesting in a given context. A monitor sphere is a spheric area surrounding a point that can be associated to different events, like the hand of a human entering into it. Using this system and the vision capabilities of the robot we can monitor interesting activities, like the fact that a human takes an object or throws it into a trashbin. The monitor spheres for a human agent are created when he enters the scene, considering object affordances. If the human doesn't have items in his hands, the supervision system will use SPARK to create a monitor sphere associated to every pickable object. After a user takes an item, monitor spheres for pickable objects will be erased and the robot will create new spheres for containers, such as thrashbins, where the user can throw its items. For the moment we consider only these two kind of affordances, but we plan to include others in the future, allowing, for example, users to place objects on furnitures, such as tables.

4. Robustness and Safety Our system incorporates different robustness and safety mechanisms. The robot can deal with failed actions by updating its knowledge of the environment and replanning accordingly. For example, if the robot tries to take an item and fails, it will update its knowledge introducing the information that the item is not reachable from the current position. The robot can then replan, for example by asking the user to take the item. The robot has the ability to stop its current action, for example because of unexpected changes in the environment. The robot is also able to pause and resume the execution of an action, for example because the arm of the human is in its planned trajectory. 5. Flexibility. Our system is designed to be generic and easily expanded. New scenarios can be added by creating a new planning domain (for HATP and the Collaboration Planners), and eventually adding new actions to the system repertoire.

Experiments

For our experiments, we present a scenario where the robot and a human have a joint goal: cleaning a set of furniture. The two partners must place the tapes present on the furniture in a trashbin. We will use two pieces of furniture, identified as TABLE 4 and IKEA SHELF and three tapes, identified as GREY TAPE, LOTR TAPE and WALLE TAPE. We will use one trashbin, named PINK TRA-SHBIN. We will place these items differently in each example, depending on our needs and won't necessary use all of them together. We will present a set of runs of the system, which show its capacities3 :

-Robot adapts: In this scenario (figure 2) the user is asked to clean the table, without agreeing before the start on a clear plan with the robot. The user is informed that the robot will try to help as it can. The user moves to the table and takes the WALLE TAPE. At this point the robot notices that the user has completed an action and understands that he wants to clean the table.

The robot creates a plan and executes its part of it while monitoring the human, which executes its part without deviating from the plan calculated by the robot. -Modality switch and user plans: In this scenario (figure 3) the robot is the only agent able to reach both tapes, but it can't reach the trashbin, which can instead be reached by the human. We tested this scenario in two different runs. In the first one we start with the robot in 'robot plans' modality. After exploring the environment the robot produces a plan and starts its execution. While the robot is taking the LOTR TAPE the human moves to take the WALLE TAPE. This deviates from the robot plan, so it switches to the 'robot adapts' modality, communicating the change to the user. The user throws the WALLE TAPE in the PINK TRASHBIN and meanwhile the robot takes the LOTR TAPE and handles it to the user. The user takes the LOTR TAPE and throws it in the PINK TRASHBIN, completing the task.

In the second run the robot is in the 'user plans' mode. The user is asked to clean the table as he wishes. The user asks the robot to take each tape and give it to him, throwing them in the trashbin.

-Replanning after failed action: In this scenario (figure 4) the robot is the only agent able to reach the trashbin, while both agents can reach the two tapes. The robot is in 'robot plans' modality and, after examining the environment, produces a plan. After taking and throwing the LOTR TAPE, the robot tries to take the WALLE TAPE, but fails because it's too far. The robot informs the user and replans. The agents execute the plan, completing the task. -Replanning after human inactivity. In this run the robot computes that the GREY TAPE and PINK TRASHBIN are reachable only by the human, while the WALLE TAPE is reachable only by the robot. The robot computes a plan and starts executing it, observing the human reactions. After an initial stage when the human is commited to the task, he doesn't execute a part of the plan (taking the final tape and throwing it), so the robot looks for another plan. The only solution to the problem is the one already computed at the beginning, so the robot decides to ask the human to take the tape and throw it. A run of this scenario is shown in figure 5.

Conclusions

The studied experiment shows that our system is able to exhibit the capacities discussed in section 3. Also, an interesting aspect of our system is that it's generic enough to be adapted to other manipulation scenarios, even involving more than one human. We review some of the main results of our experiments:

-The system is able to handle joint goals. The system is able to create shared plans with different users, taking into account the capabilities of each agent. When unexpected changes in the world or task status arise, the system is able to quickly replan, adapting to new scenarios. The system is able to execute this joint goal in a human aware way. -The system is able to handle joint actions. The system is able to estimate user intentions in collaborative tasks and to choose appropriate actions, using a set of POMDP models. -The system is able to handle user preferences. The system is able to adapt itself to user preferences, allowing the human partner to give commands or to be more passive in its role and switching from one modality to the other. -The system is able to handle each agent beliefs. The system is able to represent different belief states for different agents and to take into accout what users can see, reach and know when creating a plan. -The system is able to monitor human actions. The system is able to monitor human actions using a mechanism that is simple, but fast and efficient for the studied scenarios.

To further understand the advantages and disadvantages of these different modalities, and also in which conditions one or the others are pertinent, we need to conduct user studies, which will be done in the near future.

Fig. 2 :

 2 Fig. 2: Robot adapts.This figure shows the robot's representation of the scenario. The white tape is the WALLE TAPE, while the blue one is the LOTR TAPE. The round shapes represent the agents' rechabilities, with red shapes representing robot reachabilities and green shapes human reachabilities. In this case only the human can reach the WALLE TAPE while both agents can reach the LOTR TAPE and the PINK TRASHBIN. After the human takes the WALLE TAPE the robot produces a plan where the human must throw the tape in the thrashbin while the robot can take the LOTR TAPE and throw it in the trashbin.

Fig. 3 :

 3 Fig. 3: Modality switch and user plans. Another configuration of the environment, where the robot can reach the two tapes and the human can reach the thrashbin. The robot generates an initial plan from this situation. The block surrounding the Give and Receive actions means that they are considered a single joint action.

Fig. 4 :

 4 Fig. 4: Replanning after failed action. Here we can see a first plan, produced at the start of the scenario, and a second, produced after the robot fails to take the WALLE TAPE.

Fig. 5 :

 5 Fig.5:The picture shows a run of our 'replanning after human inactivity scenario'. The different rows show, starting from top to bottom: the real world picture, the world state representation built by the robot, symbolic facts input in the knowledge base at each time step, action taken by each agent at each time step, the current plan calculated by the robot.

Videos from our experiments can be seen at http://homepages.laas.fr/mfiore/ iser2014.html

Acknowledgments

This work was conducted within the EU SAPHARI project (www.saphari.eu) funded by the E.C. division FP7-IST under contract ICT-287513.


Fabio Gadducci
email: fabio.gadducci@di.unipi.it

Francesco Santini
email: francesco.santini@iit.cnr.it

Luis F Pino
email: luis.pino@unica.it

Frank D Valencia
email: frank.valencia@lix.polytechnique.fr

A Labelled Semantics for Soft Concurrent Constraint Programming

We present a labelled semantics for Soft Concurrent Constraint Programming (SCCP), a language where concurrent agents may synchronize on a shared store by either posting or checking the satisfaction of (soft) constraints. SCCP generalizes the classical formalism by parametrising the constraint system over an order-enriched monoid: the monoid operator is not required to be idempotent, thus adding the same information several times may change the store. The novel operational rules are shown to offer a sound and complete co-inductive technique to prove the original equivalence over the unlabelled semantics.

The research has been partially

Introduction

Concurrent Constraint Programming (CCP) [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] is a language based on a sharedmemory communication pattern: processes may interact by either posting or checking partial information, which is represented as constraints in a global store. CCP belongs to the larger family of process calculi, thus a syntax-driven operational semantics represents the computational steps. For example, the term tell(c) is the process that posts c in the store, and the term ask(c) → P is the process that executes P if c can be derived from the information in the store.

The formalism is parametric with respect to the entailment relation. Under the name of constraint system, the information recorded on the store is structured as a partial order (actually, a lattice) ≤, where c ≤ d means that c can be derived from d. Under a few requirements over such systems, CCP has been provided with (coincident) operational and denotational semantics. More recently, a labelled semantics has also been provided, and the associated weak bisimilarity proved to coincide with the original semantics [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF].

A key aspect of CCP is the idempotency of the operator for composing constraints: adding the same information twice does not change the store. On the contrary, the soft variant of the formalism (Soft CCP, or just SCCP [START_REF] Bistarelli | Soft concurrent constraint programming[END_REF]) drops idempotency: constraint systems in SCCP may distinguish the number of occurrences of a piece of information. Dropping idempotency requires a complete reworking of the theory. Although an operational semantics for SCCP has been devised [START_REF] Bistarelli | Soft concurrent constraint programming[END_REF], hitherto neither the denotational nor the labelled one has been reintroduced. This is unfortunate since due to its generality, SCCP has been successfully applied as a specification formalism for negotiation of Service Level Agreements [START_REF] Buscemi | CC-Pi: A constraint-based language for specifying service level agreements[END_REF], or the enforcement of ACL-based access control [START_REF] Bistarelli | A secure non-monotonic soft concurrent constraint language[END_REF].

The objective of our work is the development of a general theory for the operational as well as the denotational semantics of SCCP, via the introduction of suitable behavioral equivalences. Reaching this objective is technically challenging, since most of the simplicity of CCP is based precisely on the premise that posting an information multiple times is the same as posting it only once.

As a language, SCCP has been used as a specification formalism for agents collaborating via a shared knowledge basis, possibly with temporal features [START_REF] Bistarelli | Timed soft concurrent constraint programs[END_REF]. Thus, on a methodological level, the development of behavioural equivalences for SCCP may result in the improvement on the analysis techniques for agents that need to reason guided by their preferences, more so if their knowledge (e.g. of their environment) is not complete. Indeed, the paper shows that systems specified by SCCP may benefit from the feasible proof and verification methods typically associated with bisimilarity, compared with the classical analysis based on (possibly infinite) sequences of computations. This is true also whenever agents have to coordinate despite the global problem being over-constrained (i.e., admitting no solution), and simulation may serve as a powerful mechanism for distilling suitable approximated solutions. [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] establishes a denotational semantics for CCP and an equational theory for infinite agents. More recently, in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] the authors prove that the axiomatisation is underlying a specific weak bisimilarity among agents, thus providing a clear operational understanding. The key ingredients are a complete lattice as the domain of the store, with least upper bound for constraint combination, and a notion of compactness such that domain equations for the parallel composition of recursive agents would be well-defined. On the contrary, the soft version [START_REF] Bistarelli | Soft concurrent constraint programming[END_REF] drops the upper bound for combination in exchange of a more general monoidal operator. Thus, the domain is potentially just a (not necessarily complete) partial order, possibly with finite meets and a residuation operator (a kind of inverse of the monoidal one) in order to account for algorithms concerning constraint propagation. Indeed, the main use of SCCP has been in the generalisation of classical constraint satisfaction problems, hence the lack of investigation about e.g compactness and denotational semantics.

Contribution. The work in

Therefore, in this paper we connect the works on the soft [START_REF] Bistarelli | Soft concurrent constraint programming[END_REF] and the classical (also indicated in the literature as "crisp") [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF][START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] paradigm by investigating a labelled semantics for SCCP. In particular, the results will be a mix of those investigated in the two communities, namely, a monoid whose underlying set of elements form a complete lattice. We will recast the notion of compactness, and afterwards the SCCP semantics, thus making the work a direct extension of the proposal for the crisp language. We will then introduce a novel labelled semantics for SCCP which will allow us to give a sound and complete technique to prove the equivalence over the unlabelled semantics.

A Few Technical Remarks (with some novelty)

This section recalls the main notions we are going to need later on. First of all, we present some basic facts concerning monoids [START_REF] Karner | Semiring-based constraint satisfaction and optimization[END_REF] enriched over complete lattices. These are used to recast the standard presentation of the soft constraints paradigm, and to generalise the classical crisp one.

Lattice-enriched Monoids

Definition 1 (Complete lattices). A partial order (PO) is a pair A, ≤ such that A is a set of values and ≤ ⊆ A × A is a reflexive, transitive, and anti-symmetric relation. A complete lattice (CL) is a PO such that any subset of A has a least upper bound (LUB).

We denote as X the necessarily unique LUB of a subset X ⊆ A, and explicitly ⊥ and if we are considering the empty set and the whole A, respectively: the former is the bottom and the latter is the top of the PO. Obviously, CLs also have the greatest lower bound (GLB) for any subset Y ⊆ A, denoted as Y.

In the following we fix a CL C = A, ≤ .

Definition 2 (Compact elements

). An element a ∈ A is compact (or finite) if whenever a ≤ Y there exists a finite subset X ⊆ Y such that a ≤ X.

Note that for complete lattices the definition of compactness given above coincides with the one using directed subsets. It will be easier to generalise it, though, to compactness with respect to the monoidal operator (see Def. 6). We let A C ⊆ A denote the set of compact elements of C. Note that A C might be trivial. Consider e.g. the CL [0, 1], ≥ (the segment of the reals with the inverse of the usual order), used for probabilistic constraints [START_REF] Fargier | Uncertainty in constraint satisfaction problems: a probabilistic approach[END_REF]: only the bottom element 1 is compact. As we will see, the situation for the soft paradigm is more nuanced.

Definition 3 (Monoids).

A commutative monoid with identity (IM) is a triple A, ⊗, 1 where ⊗ : A×A → A is a commutative and associative function and ∀a ∈ A.⊗(a, 1) = a.

We will often use an infix notation, such as a ⊗ b for a, b ∈ A. The monoidal operator can be defined for any multi-set: it is given for a family of elements a i ∈ A indexed over a finite, non-empty set I, and it is denoted by i∈I a i . Whenever for an index set I all the a i 's are different, we write S instead of i∈I a i for the set S = {a i | i ∈ I}. Conventionally, we also denote ∅ = ⊥. We now move our attention to the domain of values we are going to consider.

Definition 4 (CL-enriched IMs).

A CL-enriched IM (CLIM) is a triple S = A, ≤, ⊗ such that A, ≤ is a CL, A, ⊗, ⊥ is an IM, and furthermore the following holds

(distributivity) ∀a ∈ A.∀X ⊆ A. a ⊗ X = {a ⊗ x | x ∈ X} Remark 1.
The reader who is familiar with the soft constraint literature may have noticed that we have basically rewritten the standard presentation using a CLIM instead of an absorptive semiring, recently popularized as c-semiring [START_REF] Bistarelli | Semiring-based constraint satisfaction and optimization[END_REF], where the a ⊕ b operator is replaced by the binary LUB a ∨ b. Besides what we consider a streamlined presentation, the main advantage in the use of CLIMs is the easiness in defining the LUB of infinite sets and, as a consequence, the notion of ⊗-compactness given below. An alternative solution using infinite sums can be found in [14, Section 3], and a possible use is sketched in [START_REF] Bistarelli | Enhancing constraints manipulation in semiring-based formalisms[END_REF].

Thanks to distributivity, we can show that ⊗ is monotone, and since ⊥ is the identity of the monoid, monotonicity implies that the combination of constraints is increasing, i.e., ∀a, b ∈ A.a ≤ a ⊗ b holds. Finally, we recall that by definition ∅ = , so that ∀a ∈ A.a ⊗ = also holds. 5In the following, we fix a CLIM S = A, ≤, ⊗ . The next step is to provide a notion of infinite composition. Our definition is from [START_REF] Karner | Semiring-based constraint satisfaction and optimization[END_REF] (see also [14, p. 42]).

Definition 5 (Infinite composition).

Let I be a (countable) set of indexes. Then, composition i∈I a i is given as J⊆I j∈J a j for all finite subsets J.

Should I be finite, the definition gives back the usual multiset composition, since ⊗ is monotone and increasing. Indeed, as the infinitary composition is also monotone and increasing, and by construction A = A = holds. We now provide a notion of compactness with respect to the monoidal operator.

Definition 6 (⊗-compact elements

). An element a ∈ A is ⊗-compact (or ⊗-finite) if whenever a ≤ i∈I a i then there exists a finite subset J ⊆ I such that a ≤ j∈J a j .

We let A ⊗ ⊆ A denote the set of ⊗-compact elements of S. It is easy to show that a compact element is also ⊗-compact, i.e. A C ⊆ A ⊗ . Indeed, the latter notion is definitively more flexible. Consider e.g. the CLIM [0, 1], ≥, × examined above, which corresponds to the segment of the reals with the inverse of the usual order and multiplication as monoidal product. Since any infinite multiplication tends to 0, then all the elements are ⊗-compact, except the top element itself, that is, precisely 0.

Remark 2. It is easy to show that idempotency implies that coincides with LUBs, that is, S = S for all subsets S ⊆ A. In other words, the whole soft structure collapses to a complete distributive lattice. Indeed, requiring distributivity makes the soft paradigm not fully comparable with the crisp one. We are going to discuss it again in the concluding remarks.

Some Operators: Residuation and Cylindrification

We close this section by presenting two operators on CL-enriched IMs.

The first is a simple construction for building a weak inverse of the monoidal operator in CL-enriched monoids, known in the literature as residuation [START_REF] Golan | Semirings and Affine Equations over Them: Theory and Applications[END_REF][START_REF] Galatos | Residuated Lattices: An Algebraic Glimpse at Substructural Logics[END_REF]. Most important for our formalism is the following result on ⊗-compactness.

Lemma 1. Let a, b ∈ A. If a is ⊗-compact, so is a ÷ b. Proof. If a ÷ b ≤ i∈I a i , then by monotonicity a ≤ i∈I { * } a i for a * = b.
By ⊗compactness of a there exists a finite J ⊆ I such that a ≤ j∈J { * } a j , and by the definition of division a ÷ b ≤ j∈J a j , hence the result holds.

Most standard soft instances (boolean, fuzzy, probabilistic, weighted, and so on) are described by CL-enriched monoids and are residuated: see e.g. [START_REF] Bistarelli | Enhancing constraints manipulation in semiring-based formalisms[END_REF]. For these instances the ÷ operator is used to (partially) remove constraints from the store, and as such is going to be used in Section 4. In fact, in the soft literature it is required a tighter relation of (full) invertibility, also satisfied by all the previous CLIMs instances, stated in our framework by the definition below.

Definition 8. A CLIM S is invertible if b ≤ a implies b ⊗ (a ÷ b) = a for all a, b ∈ A ⊗ .
We now consider two families of operators for modelling the hiding of local variables and the passing of parameters in soft CCP. They can be considered as generalised notions of existential quantifier and diagonal element [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF], which are expressed in terms of operators of cylindric algebras [START_REF] Monk | An introduction to cylindric set algebras[END_REF]. 6Definition 9 (Cylindrification). Let V be a set of variables. A cylindric operator ∃ over S and V is given by a family of monotone, ⊗-compactness preserving functions

∃ x : A → A indexed by elements in V such that for all a, b ∈ A and x, y ∈ V 1. ∃ x a ≤ a; 2. ∃ x (a ⊗ ∃ x b) = ∃ x a ⊗ ∃ x b; 3. ∃ x ∃ y a = ∃ y ∃ x a. Let a ∈ A. The support of a is the set of variables sv(a) = {x ∈ V | ∃ x a a}.
For a finite X ⊆ V we denote by ∃ X a any sequence of function applications. Also, we fix a set of variables V and a cylindric operator ∃ over CLIM S and V.

Definition 10 (Diagonalisation).

A diagonal operator δ for ∃ is given by a family of idempotent elements δ x,y ∈ A indexed by pairs of elements in V such that δ x,y = δ y,x and for all a ∈ A and x, y, z

∈ V 1. δ x,x = ⊥; 2. if z {x, y} then δ x,y = ∃ z (δ x,z ⊗ δ z,y ); 3. if x y then a ≤ δ x,y ⊗ ∃ x (a ⊗ δ x,y ).
Axioms 1 and 2 above plus idempotency imply that ∃ x δ x,y = ⊥, which in turn implies (again with axiom 2 and idempotency of ∃) that sv(δ x,y ) = {x, y} for x y. Diagonal operators are going to be used for modelling variable substitution and parameter passing. In the following, we fix a diagonal operator δ for ∃.

Definition 11 (Substitution). Let x, y ∈ V and a ∈ A. The substitution a[ y / x ] is defined as a if x = y and as ∃ x (δ x,y ⊗ a) otherwise.

We now rephrase some of the laws holding for the crisp case (see [1, p.140]).

Lemma 2. Let x, y ∈ V and a ∈ A. Then it holds 1. y sv(a) implies (a[ y / x ])[ x / y ] = a; 2. a[ y / x ] ⊗ b[ y / x ] = (a ⊗ b)[ y / x ]; 3. x sv(a[ y / x ]). Proof. Consider e.g. the most difficult item 2. By definition a[ y / x ] ⊗ b[ y / x ] = ∃ x (δ x,y ⊗ a) ⊗ ∃ x (δ x,y ⊗ b), which in turn coincides with ∃ x (δ x,y ⊗ a ⊗ ∃ x (δ x,y ⊗ b)) by axiom 2 of ∃; by axiom 3 of δ x,y we have that (a ⊗ b)[ y / x ] = ∃ x (δ x,y ⊗ a ⊗ b) ≤ ∃ x (δ x,y ⊗ a ⊗ ∃ x (δ x,y ⊗ b))
, while the vice versa holds by the monotonicity of ∃ x .

Deterministic Soft CCP

We now introduce our language. We fix an invertible CLIM S = C, ≤, ⊗ , which is also cylindric over a set of variables V, denoting by c an element in C ⊗ .

A stop | tell(c) | ask(c) → A | A A | ∃ x A | p(x).
Let A be the set of all agents, which is parametric with respect to a set P of (unary) procedure declarations p(x) = A such that f v(A) = {x}. 7In Tab. 1 we provide a reduction semantics for SCCP: a pair Γ, → , for Γ = A × C ⊗ the set of configurations and -→ ⊆ Γ × Γ a family of binary relations indexed over set of variables, i.e., -→= ∆⊆V -→ ∆ and -→ ∆ ⊆ Γ × Γ.

In R1 a constraint c is added to the store σ. R2 checks if c is entailed by σ: if not, the computation is blocked. Rules R3 and R4 model the interleaving of two agents in parallel. Rule R5 replaces a procedure identifier with the associated body, renaming the formal parameter with the actual one: A[ y / x ] stands for the agent obtained by replacing all the occurrences of x with y. 8 Rule R6 hides the variable x occurring in A. The variable w that replaces x is globally fresh, as ensured by requiring w ∆. The latter is more general than just requiring that 9We denote f v(A) ∪ sv(σ) as f v(γ) for a configuration γ = A, σ , and by γ[ z / w ] the component-wise application of substitution [ z / w ]. Clearly γ → ∆ γ implies f v(γ) ⊆ ∆, and we now further provide three lemmata on reduction.

R1 sv(σ) ∪ sv(c) ⊆ ∆ tell(c), σ -→ ∆ stop, σ ⊗ c Tell R3 A, σ -→ ∆ A , σ ∧ f v(B) ⊆ ∆ A B, σ -→ ∆ A B, σ Par1 R5 {y} ∪ sv(σ) ⊆ ∆ ∧ p(x) = A ∈ P p(y), σ -→ ∆ A[ y / x ], σ Rec R2 c ≤ σ ∧ sv(σ) ∪ sv(c) ⊆ ∆ ask(c) → A, σ -→ ∆ A, σ Ask R4 A, σ -→ ∆ A , σ ∧ f v(B) ⊆ ∆ B A, σ -→ ∆ B A , σ Par2 R6 f v(A) ∪ sv(σ) ⊆ ∆ ∧ w ∆ ∃ x A, σ -→ ∆ A[ w / x ], σ
w f v(A) ∪ sv(σ), since B, ρ -→ ∆ implies that f v(B) ∪ sv(ρ) ⊆ ∆.

Lemma 3 (Mono).

Let A, σ → ∆ B, σ be a reduction. Then, σ ≤ σ and sv(σ ) ⊆ ∆.

The proof is straightforward: only rule R1 can modify the store, and σ ≤ σ ⊗ c as well as sv(σ⊗c) ⊆ sv(σ)∪sv(c) hold, since as shown above f v(tell(c))∪sv(σ) ⊆ ∆.

Lemma 4 (Operational mono)

. Let A, σ → ∆ B, σ be a reduction and ρ ∈ C ⊗ such that sv(ρ) ⊆ ∆. Then, there exists a reduction A, σ ⊗ ρ → ∆ B, σ ⊗ ρ .
The proof is straightforward, since as before sv(σ ⊗ ρ) ⊆ sv(σ) ∪ sv(ρ) and moreover σ, ρ ∈ C ⊗ ensure that σ ⊗ ρ ∈ C ⊗ .

Observational Semantics

To define fair computations (Def. 12), we introduce enabled and active agents. Note that any transition is generated by an agent of the shape tell(c) or ask(c) → A or p(x) or ∃ x A via the application of precisely one instance of one of the axioms R1, R2, R5, and R6 of Tab. 1. An agent of such shape is active in a transition t = γ → γ if it generates such transition, i.e. if there is a derivation of t where that agent is used in the building axiom. Moreover, an agent is enabled in a configuration γ if there is a transition γ → γ such that the agent is active in it.

Definition 12 (Fair computations). Let γ

0 → ∆ 1 γ 1 → ∆ 2 γ 2 → ∆ 3 .
. . be a (possibly infinite) computation. It is fair if it is increasing (i.e., ∆ k ⊆ ∆ k+1 for any k) and whenever an agent A is enabled in some γ i then A is active in γ j → ∆ j+1 γ j+1 for some j ≥ i.

Note that fairness is well given: the format of the rules allows us to always trace the occurrence of an agent along a computation.

Definition 13 (Observables). Let

ξ = γ 0 → ∆ 1 γ 1 → ∆ 2 . . . be a (possibly infinite) computation with γ i = A i , σ i . Result(ξ) is i (∃ X i σ i ), for X i = ( f v(γ i )) \ ( f v(γ 0 )).
Similarly to crisp programming [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF], if a finite computation is fair then it is deadlocked and its result coincides with the store of the last configuration.

Proposition 1 (Confluence). Let γ be a configuration and ξ 1 , ξ 2 two (possibly infinite) computations of γ. If ξ 1 and ξ 2 are fair, then Result(ξ 1 ) = Result(ξ 2 ).

The proposition is an immediate consequence of the lemma below.

Lemma 5. Let γ → ∆ i γ i be reductions for i = 1, 2. Then one of the following holds

1. ξ i = γ → ∆ i γ i [ z / w i ] and γ 1 [ z / w 1 ] = γ 2 [ z / w 2 ] for w i ∆ i and z fresh; 2. ξ i = γ → ∆ i γ i [ z i / w i ] → ∆ 1 ∪∆ 2 ∪{z i } γ 3 for w i (∆ 1 ∩ ∆ 2 ) ∪ f v(γ 3
) and z i 's fresh.

In both cases, Result(ξ 1 ) = Result(ξ 2 ).

Proof. First of all, note that the calculus is deterministic except for the parallel and the hiding operators. Consider the latter. The problem may arise if different fresh variables are chosen, let us say w 1 and w 2 . However,

γ 1 [ z / w 1 ] = γ 2 [ z / w 2 ]
by replacing the new variables with a globally fresh one, as in item 1.

So, let us assume that the two reductions occur on the opposite sides of a parallel operator. Also, let γ → ∆ 1 γ 1 replace a hiding operator with a variable w 1 (hence we have w 1 ∆ 1 ). If w 1 ∈ f v(γ 2 ), since w 1 γ and the only reduction enlarging the set of free variables is the replacement of a hiding operator, also γ → ∆ 2 γ 2 must replace a hiding operator with variable w 1 , and thus it suffices to replace w 1 with fresh variables z 1 and z 2 in the two reductions, in order for item 2 to be verified. If w 1 f v(γ 2 ), then ξ 2 is obtained by replacing in γ 2 the hiding operator with z 1 instead of w 1 . As for obtaining ξ 1 , the only problematic case is if γ → ∆ 2 γ 2 also replaces a hiding operator with a variable w 2 ∈ ∆ 1 ∪ f v(γ 1 ). However, we have that w 2 f v(γ 1 ) since otherwise (as shown above) w 1 = w 2 , thus ξ 1 is obtained by replacing in γ 1 the hiding operator with z 2 instead of w 2 , and item 2 is then verified.

Among the remaining cases, the only relevant one is whenever both actions add different constraints to the store. So, let us assume that γ

= A 1 A 2 , σ such that A 1 , σ → ∆ 1 B 1 , σ 1 and A 2 , σ → ∆ 2 B 2 , σ 2 .
Note that since reduction semantics is monotone (Lemma 3) and σ is ⊗-compact, also σ 1 is ⊗-compact and furthermore we have

σ 1 = σ ⊗ (σ 1 ÷ σ). Now, operational monotonicity (Lemma 4) ensures us that B 1 A 2 , σ ⊗ (σ 1 ÷ σ) → ∆ 1 ∪∆ 2 B 1 B 2 , σ ⊗ (σ 1 ÷ σ) ⊗ (σ 2 ÷ σ)
and by symmetric reasoning the latter configuration is the one we were looking for.

The result above is a local confluence theorem, which is expected, since the calculus is essentially deterministic. The complex formulation is due to the occurrence of hiding operators: as an example, different fresh variables may be chosen for replacing ∃ x , such as w 1 and w 2 in the first item above, and then a globally fresh variable z has to be found for replacing them.

As a final remark, note that γ → ∆ γ with z ∈ f v(γ) and w f v(γ ) implies γ[ w / z ] → (∆\{z})∪{w} γ [ w / z ]. Combined with the proposition above, they ensure that fair computations originating from a configuration are either all finite or all infinite, and furthermore they have the same result. So, in the following we denote as Result( A, σ ) the unique result of the fair computations originating from A, σ . This fact allows to define an observation-wise equivalence.

Definition 14 (Observational equivalence). Let A, B ∈ A be agents. They are observationally equivalent (

A ∼ o B) if Result( A, σ ) = Result( B, σ ) for all σ ∈ C ⊗ .
It is easily shown that ∼ o is preserved by all contexts, i.e., it is a congruence. 10

Saturated Bisimulation

As proposed in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] for crisp languages, we define a barbed equivalence between two agents [START_REF] Milner | Barbed bisimulation[END_REF]. Since barbs are basic observations (predicates) on the states of a system, in this case they correspond to the compact constraints in C ⊗ , and we say that A, σ verifies c, or that A, σ ↓ c holds, if c ≤ σ. However, since barbed bisimilarity is an equivalence already for CCP, along [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] we propose the use of saturated bisimilarity in order to obtain a congruence: Defs. 15 and 16 respectively provide the strong and weak definition of saturated bisimilarity.

Definition 15 (Saturated bisimilarity). A saturated bisimulation is a symmetric relation R on configurations such that whenever (

A, σ , B, ρ ) ∈ R 1. if A, σ ↓ c then B, ρ ↓ c ; 2. if A, σ -→ γ 1 then there exists γ 2 such that B, ρ -→ γ 2 and (γ 1 , γ 2 ) ∈ R; 3. ( A, σ ⊗ d , B, ρ ⊗ d ) ∈ R for all d ∈ C ⊗ .
We say that γ 1 and γ 2 are saturated bisimilar (γ 1 ∼ s γ 2 ) if there exists a saturated bisimulation R such that (γ 1 , γ 2 ) ∈ R. We write A ∼ s B if A, ⊥ ∼ s B, ⊥ .

We now let -→ * denote the reflexive and transitive closure of -→, restricted to increasing computations. We say that γ ⇓ c holds if there exists γ = A, σ such that γ -→ * γ and c ≤ ∃ X σ for X = f v(γ ) \ f v(γ).

Definition 16 (Weak saturated bisimilarity).

Weak saturated bisimilarity (≈ s ) is obtained from Def. 15 by replacing -→ with -→ * and ↓ c with ⇓ c .

Since ∼ s (and ≈ s ) is itself a saturated bisimulation, it is obvious that it is upward closed, and it is also a congruence with respect to all the contexts of SCCP (i.e., it is preserved under any context): indeed, a context C[•] can modify the behaviour of a configuration only by adding constraints to its store. 10 Recall that a context C[•] is a syntactic expression with a single hole • such that replacing • with an agent A in the context produces an agent, denoted by

C[A]. For example if C[•] is the context tell(c) • then C[A] = tell(c) A. An equivalence between agents is a congruence if A B implies C[A] C[B] for every context C[•].
We now show that ≈ s , as given in Def. [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF], coincides with the observational equivalence ∼ o (see Def. 14). First we recall the notion of and a classic result on cofinality: two (possibly infinite) chains c 0 ≤ c 1 ≤ . . . and d 0 ≤ d 1 ≤ . . . are said to be cofinal if for all c i there exists a d j such that c i ≤ d j and, viceversa, for all d i there exists a c j such that d i ≤ c j . Lemma 6. Let c 0 ≤ c 1 ≤ . . . and d 0 ≤ d 1 ≤ . . . be two chains. (1) If they are cofinal, then they have the same limit, i.e., i c i = i d i . (2) If the elements of the chains are ⊗-compact and i c i = i d i , then the two chains are cofinal.

Proof. Let us tackle (2), and consider the sequence e 0 = c 0 and e i = c i+1 ÷ c i . Each e i is the difference between two consecutive elements of a chain. Since the CLIM is invertible we have c k = i≤k e i and thus i c i = i e i . Since each d j is ⊗compact and d j ≤ i e i , there is a k such that d j ≤ i≤k e i . The same reasoning is applied to the chain d 0 ≤ d 1 ≤ . . . , thus the result holds.

For proving Proposition 2 we now relate weak barbs and fair computations.

Lemma 7. Let ξ = γ 0 -→ γ 1 -→ γ 2 -→ . . . be a (possibly infinite) fair computation. If γ 0 ⇓ d then there exists a store σ i in ξ such that d ≤ ∃ X i σ i for X i = f v(γ i ) \ f v(γ 0 ).
The lemma holds since the language is deterministic and computations fair.

Proposition 2. A ∼ o B if and only if

A ≈ s B.
Proof. The proof proceeds as follows.

From ≈ s to ∼ o . Assume A, ⊥ ≈ s B, ⊥ and take a ⊗-compact c ∈ C ⊗ . Let A, c -→ A 0 , σ 0 -→ A 1 , σ 1 -→ . . . -→ A n , σ n . . . -→ . . . (1)
B, c -→ B 0 , ρ 0 -→ B 1 , ρ 1 -→ . . . -→ B n , ρ n . . . -→ . . . (2)
be two fair computations. Since ≈ s is upward closed, A, c ≈ s B, c and thus B, c ⇓ σ i for all σ i . By Lemma 7, it follows that there exists an ρ j (in the above computation) such that ∃ Γ i σ i ≤ σ i ≤ ∃ Γ j ρ j , and analogously for all ρ i . Then σ 0 ≤ σ 1 ≤ . . . and ρ 0 ≤ ρ 1 ≤ . . . are cofinal and by Lemma 6, it holds

that i ∃ Γ i σ i = i ∃ Γ i ρ i , which means Result( A, c ) = Result( B, c ). From ∼ o to ≈ s . Assume A ∼ o B.
A ∼ o B, then i ∃ Γ i σ i = i ∃ Γ j ρ i .
Since all (the projections of) the intermediate stores of the computations are ⊗-compact, then by Lemma 6, for all σ i there exists an ρ j such that Although ≈ s is fully abstract, it is to some extent unsatisfactory because of the upward-closure, namely, the for-all quantification in condition 3 of Def. 16.

∃ Γ i σ i ≤ ∃ Γ j ρ j . Now suppose that A, c ⇓ d . By Lemma 7, there exists a σ i such that d ≤ ∃ Γ i σ i . Thus B, c ⇓ d . It is now easy to prove that R = {(γ 1 , γ 2 ) | ∃c. A, c -→ * γ 1 & B, c -→ * γ 2 } is a weak saturated bisimulation (Def. 16). Take (γ 1 , γ 2 ) ∈ R. If γ 1 ⇓ d then A, c
In Tab. 2 we refine the notion of transition (given in Tab. 1) by adding a label that carries additional information about the constraints that cause the reduction. Hence, we define a new labelled transition system (LTS) obtained by the family of relations α -→ ∆ ⊆ Γ × Γ indexed over C ⊗ , 2 V ; as a reminder, Γ is the set of configurations, C ⊗ the set of ⊗-compact constraints, and, as for the unlabelled semantics in Section 3, transitions are indexed by sets of variables. Rules in Tab. 2 are identical to those in Tab. 1, except for a constraint α that represents the minimal information that must be added to σ in order to fire an action from A, σ to A , σ , i.e., A, σ ⊗ α -→ ∆ A , σ .

LR1 sv(σ) ∪ sv(c) ⊆ ∆ tell(c), σ ⊥ --→ ∆ stop, σ ⊗ c Tell LR3 A, σ α - → ∆ A , σ ∧ f v(B) ⊆ ∆ A B, σ α - → ∆ A B, σ Par1 LR5 {y} ∪ sv(σ) ⊆ ∆ ∧ p(x) = A ∈ P p(y), σ ⊥ -→ ∆ A[ y / x ], σ Rec LR2 sv(σ) ∪ sv(c) ⊆ ∆ ask(c) → A, σ c ÷ σ ---→ ∆ A, σ ⊗ (c ÷ σ) Ask LR4 A, σ α - → ∆ A , σ ∧ f v(B) ⊆ ∆ B A, σ α - → ∆ B A , σ Par2 LR6 f v(A) ∪ sv(σ) ⊆ ∆ ∧ w ∆ ∃ x A, σ ⊥ -→ ∆ A[ w / x ],
σ Hide Table 2. An LTS for SCCP.

Rule LR2 says that ask(c) → A, σ can evolve to A, σ⊗α if the environment provides a minimal constraint α that added to the store σ entails c, i.e., α = c ÷ σ. Notice that, differently from [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], here the definition of this minimal label comes directly from a derived operator of the underlying CLIM (i.e., from ÷ ), which by Lemma 1 preserves ⊗-compactness.

The LTS is sound and complete with respect to the unlabelled semantics.

Lemma 8 (Soundness). If

A, σ α -→ ∆ A , ρ then A, σ ⊗ α -→ ∆ A , ρ .
Proof. We proceed by induction on (the depth) of the inference of A, σ α -→ ∆ A , ρ . We consider LR2: the other cases are easier to verify.

Using

LR2 then A = (ask(c) → A ), α = c ÷ σ and ρ = (σ ⊗ (c ÷ σ)) = (σ ⊗ α). We know that c ≤ (σ ⊗ (c ÷ σ)) then by using R2 A, σ ⊗ α -→ ∆ A , ρ . Lemma 9 (Completeness). If A, σ ⊗ d -→ ∆ A , ρ then there exist α, a ∈ C ⊗ such that A, σ α -→ ∆ A , ρ and α ⊗ a = d and ρ ⊗ a = ρ.
Proof. We proceed by induction on (the depth) of the inference of A, σ ⊗ d -→ ∆ A , ρ . We consider LR2: The other cases are easier to verify.

Using LR2 then A = ask(c) → A , ρ = σ ⊗ d and c ≤ ρ. Now consider A, σ α -→ ∆ A , ρ , where α = (c ÷ σ) ≤ d and ρ = (σ ⊗ α). Take a = d ÷ (c ÷ σ) then we can check that the conditions verify. First by invertibility α ⊗ a = (c ÷ σ) ⊗ (d ÷ (c ÷ σ)) = d and finally ρ ⊗ a = σ ⊗ α ⊗ a = σ ⊗ d = ρ. Theorem 1. A, σ ⊥ --→ ∆ A , σ if and only if A, σ -→ ∆ A , σ .
Strong and Weak Bisimilarity on the LTS. We now proceed to define an equivalence that characterises ∼ s without the upward closure condition. Differently from languages such as Milner's CCS, barbs cannot be removed from the definition of bisimilarity because they cannot be inferred by the transitions.

Definition 17 (Strong bisimilarity).

A strong bisimulation is a symmetric relation R on configurations such that whenever (γ 1 , γ 2 ) ∈ R with γ 1 = A, σ and γ 2 = B, ρ

1. if γ 1 ↓ c then γ 2 ↓ c , 2. if γ 1 α --→ γ 1 then ∃γ 2 such that B, ρ ⊗ α -→ γ 2 and (γ 1 , γ 2 ) ∈ R.
We say that γ 1 and γ 2 are strongly bisimilar (γ 1 ∼ γ 2 ) if there exists a strong bisimulation R such that (γ 1 , γ 2 ) ∈ R.

Whenever σ and ρ are ⊗-compact elements, the first condition is equivalent to require σ ≤ ρ. Thus (γ 1 , γ 2 ) ∈ R would imply that γ 1 and γ 2 have the same store. As for the second condition, we adopted a semi-saturated equivalence, introduced for CCP in [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF]. In the bisimulation game a label can be simulated by a reduction including in the store the label itself.

Definition 18 (Weak bisimilarity).

A weak bisimulation is a symmetric relation R on configurations such that whenever (γ 1 , γ 2 ) ∈ R with γ 1 = A, σ and γ 2 = B, ρ

1. if γ 1 ↓ c then γ 2 ⇓ c , 2. if γ 1 α --→ γ 1 then ∃γ 2 such that B, ρ ⊗ α -→ * γ 2 and (γ 1 , γ 2 ) ∈ R.
We say that γ 1 and γ 2 are weakly bisimilar (γ 1 ≈ γ 2 ) if there exists a weak bisimulation R such that (γ 1 , γ 2 ) ∈ R.

With respect to the weak equivalence for crisp constraints, some of its characteristic equivalences do not hold, so that e.g. ask(c) → tell(c) stop. As usual, this is linked to the fact that the underlying CLIM may not be idempotent.

We can now conclude by proving the equivalence between ∼ s and ∼ and between ≈ s and ≈ (hence, ≈ is further equivalent to ∼ o , using Proposition 2). We start by showing that ∼ is preserved under composition.

Lemma 10. If A, σ ∼ B, ρ , then A, σ ⊗ a ∼ B, ρ ⊗ a for all a ∈ C ⊗ .
Proof. We need to show that R = {( A, σ⊗a ∼ B, ρ⊗a ) | A, σ ∼ B, ρ } satisfies the two properties in Def. 17. i) From the hypothesis A, σ ∼ B, ρ , we have that ρ = σ, thus A, σ ⊗ a and B, ρ ⊗ a satisfy the same barbs. ii) Supposing A, σ ⊗ a ii) Suppose that A, σ → A , σ . By Theorem 1 we have A, In order to prove the correspondence between weak bisimulations, we need a result analogous to Lemma 10. The key issue is the preservation of weak barbs by the addition of constraints to the store, which is trivial in strong bisimulation.

σ ⊥ --→ A , σ . Since A, σ ∼ B, ρ , then B, ρ ⊗ ⊥ → B , ρ with A , σ ∼ B , ρ . Since ρ = ρ ⊗ ⊥, we have B, ρ → B , ρ . iii) By Lemma 10, ( A, σ ⊗ c , B, ρ ⊗ c ) ∈ R for all c ∈ C ⊗ . From ∼ sb to ∼. We show that R = {( A, σ , B, ρ ) | A, σ ∼ sb B, ρ }
Lemma 11. Let A, σ ≈ B, ρ and a, c ∈ C ⊗ . If A, σ ⊗ a ↓ c , then B, ρ ⊗ a ⇓ c . Proof. If A, σ ⊗ a ↓ c , then c ≤ σ ⊗ a. Since A, σ ≈ B, ρ and A, σ ↓ σ , then there exists B , ρ such that B, ρ → * B , ρ and σ ≤ ∃ Γ ρ for Γ = f v( B , ρ ) \ f v( B, ρ ).
Let us assume, without loss of generality, that Γ ∩ (sv(a)) = ∅; since reductions are operationally monotone (Lemma 4), we have B, ρ⊗a

→ * B , ρ ⊗ a . Finally, c ≤ σ ⊗ a = σ ⊗ ∃ Γ a ≤ ∃ Γ ρ ⊗ ∃ Γ a ≤ ∃ Γ (ρ ⊗ a), hence B, ρ ⊗ a ⇓ c .
The result below uses Lemma 11 and a rephrasing of the proof of Lemma 10 Lemma 12. If A, σ ≈ B, ρ , then A, σ ⊗ a ≈ B, ρ ⊗ a for all a ∈ C ⊗ . Theorem 3. ≈ s = ≈ Labelled versus saturated semantics. The main appeal of saturated semantics resides in always being a congruence and, in fact, the minimal congruence contained in standard bisimulation [START_REF] Montanari | Dynamic congruence vs. progressing bisimulation for CCS[END_REF]. The main drawback of this approach is that it is in principle necessary to check the behaviour of a process under every context. The problem is somewhat mitigated for SCCP, since it suffices to close the store with respect to any possible compact element (item 3 of Def. 15). At the same time, checking the feasibility of a reduction may require some computational effort, either for solving the combinatorial problem associated with calculating σ ⊗ d, or for verifying if c ≤ σ, as with agent ask(c) → A. This is the reason for searching labelled semantics and suitable notions of bisimilarity that may alleviate such a burden. The key intuition is to consider labels which somehow represent the "minimal context allowing a process to reduce", so that a bisimilarity-checking algorithm in principle needs to verify this minimal context only, instead of every one. The idea has been exploited in the simpler framework of crisp CCP [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF], and it is based on [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF]. In order to prove that γ ≈s γ , instead, we surely need to consider an infinite relation. Indeed, the smallest saturated bisimulation equating the two configuration is given by the relation below The relation above clearly is a saturated bisimulation, but any naive automatic check for that property might involve rather complex calculations.

Another reason for the complexity of checking saturated bisimilarity is the need of considering the closure -→ * of the reduction relation, which may cause a combinatorial explosion. Think e.g. of the agents i∈I ask(c i ) → stop and stop. Of course, they might be proved equivalent by exploiting the fact that saturated bisimilarity is a congruence, and by verifying that stop A ≈s A for all the agents A. A direct proof would instead require a check for each store of the reductions arising from all the possible interleaving of the c i elements.

Towards an Axiomatisation for Weak Bisimilarity

Once the behaviour of an agent is captured by an observational equivalence, it is natural to look for laws characterizing it. Given its correspondence with the standard equivalence via fair computations, weak bisimilarity is the preferred behavioural semantics for soft CCP. A sound and complete axiomatisation was proposed for CCP in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. Unfortunately, the lack of idempotence in the soft formalism makes unsound some of the axioms presented in that classical paper.

ask(c)

→ stop = stop (1) tell(⊥) = stop (2) ask(⊥) → A = A (3) A stop = A (4)
A B = B A (5) A (B C) = (A B) C (6) tell(c) tell(d) = tell(c ⊗ d) (7) ask(c) → (A B) = (ask(c) → A) (ask(c) → B) (8) ∃ x tell(c) = tell(∃ x c) (9) ∃ x (ask(c) → A) = ask(∀ x c) → ∃ x A (10)
∃ x (tell(c) i∈I ask(c i ) → tell(d i )) = tell(∃ x c) ∃ x ( i∈I ask(c ⇒ x c i ) → tell(d i )) (11)
Fig. 1. Axioms for simple agents (1-8) and for agents with quantifiers [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF][START_REF] Buscemi | CC-Pi: A constraint-based language for specifying service level agreements[END_REF][START_REF] Dal Lago | Phase semantics and decidability of elementary affine logic[END_REF].

Consider e.g. the law ask(c) → ask(d) → tell(e) = ask(c ⊗ d) → tell(e), denoted as L3 in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF], and let us assume that c = d. Since c c ⊗ c, only the agent in the left-hand side of the law is guaranteed to add e, starting from a store σ such that c ≤ σ. On a similar note, most of the axioms in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] involving the parallel composition also do not hold, since as a general remark posting a constraint twice is different from adding it just once. 11We now introduce a set of sound axioms for SCCP in Figure 1. As for those of CCP in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF], they rely on an additional operator which is intuitively the dual of the existential quantifier of cylindric algebras.

Definition 19 (Co-cylindrification).

Let V be a set of variables. A co-cylindric operator ∀ over S and V is given by a family of monotone, ⊗-compactness preserving functions ∀ x : A → A indexed by elements in V such that for all a, b ∈ A and x ∈ V 1. ∀ x a ≤ b if and only if a ≤ ∃ x b.

If the ∀ operators play the role of universal quantifiers, a further family of operators had been introduced in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] for providing the role of implication, in order to provide a complete set of axioms for CCP. In our context, such an operator can be derived by means of residuation.

Lemma 13. Let a, b, c ∈ C, x ∈ V and a ⇒ x b = ∃ x a ⊗ ∀ x (b ÷ a). Then, b ≤ a ⊗ ∃ x c if and only if a ⇒ x b ≤ ∃ x a ⊗ ∃ x c.
Clearly, a ⇒ x b ∈ C ⊗ if a and b do. These properties for a ⇒ x b are the immediate extensions of those holding for the crisp setting. Exploiting cocylindrification and the latter operator we can now state Eq. 10 and Eq. 11. In Eqs. 1-3 we present the axioms related to ask and tell. Axioms on parallel composition are instead represented in Eqs. 4-6. In Eqs. 7-8 we show how adding two constraints and prefixing distributes though parallel composition. Proposition 3. Axioms 1-11 in Figure 1 are sound with respect to weak bisimilarity.

As for completeness, again the lack of idempotency made it impossible to rest the proof schema adopted for the CCP case, since the normal form exploited in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] for proving completeness cannot be lifted to SCCP agents.

Conclusions and Further Work

Inspired by [START_REF] Aristizábal | Deriving labels and bisimilarity for concurrent constraint programming[END_REF] that investigated the crisp variant of the language, in this paper we studied the behavioural semantics of the deterministic fragment of soft CCP [START_REF] Bistarelli | Soft concurrent constraint programming[END_REF], and proposed a sound axiomatisation in the spirit of [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF].

Using residuation theory (as e.g. in [START_REF] Bistarelli | Enhancing constraints manipulation in semiring-based formalisms[END_REF] for soft constraints problems) provides an elegant way to define the minimal information that enables the firing of actions in the LTS shown in Sec. 4. This choice allowed for the study of the observational equivalence of agents in terms of weak and strong bisimilarity on such LTS, and it allowed for relating them to the corresponding barbed bisimilarities of (unlabelled) reductions and with the standard semantics via fair computations. The two kinds of equivalences, as well as the sound axiomatisation for weak bisimilarity, are presented in this paper for the first time.

For future work, we plan to provide a complete axiomatisation and a denotational semantics for soft CCP by building on the work for the crisp case in [START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF]. Concerning the axioms, we will try and investigate the relationship between soft CCP and a logical system whose fundamental properties are closely related to the ones we have investigated in this paper; namely affine linear logic [START_REF] Dal Lago | Phase semantics and decidability of elementary affine logic[END_REF]. This logical system rejects contraction but admits weakening, which intuitively correspond to dropping idempotence and preserving monotonicity in the soft formalism. The denotational model of CCP is based on closure operators: Each agent is compositionally interpreted as a monotonic, extensive and idempotent operator/function on constraints. We shall then investigate a denotational model for soft CCP processes based on pre-closure operators [START_REF] Arkhangelskii | General Topology I[END_REF] (or Čech closure operators), i.e., closure operators that are not required to be idempotent.

Finally, we plan to consider two extensions of the language, checking how far the results given in this paper can be adapted. As evidenced by [START_REF] Pino | A behavioral congruence for concurrent constraint programming with non-deterministic choice[END_REF] a non-deterministic extension is an interesting challenge since the closure under any context for the saturated bisimilarity gets more elaborated than just closing with respect to the addition of constraints (Defs. 15 and 16, condition 3), and similarly one also needs to find the right formulation of bisimilarity for the labelled transitions systems. Also, the presence of residuation makes intuitive the definition of a retract operator for the calculus. Even if the operational semantics would be less affected, retraction would require a complete reformulation of the denotational semantics via fair computations, since monotonicity (as stated in Lemma 3) would not hold anymore [START_REF] Bistarelli | A secure non-monotonic soft concurrent constraint language[END_REF]. Finally, we might consider languages with temporal features, such as timed SCCP [START_REF] Bistarelli | Timed soft concurrent constraint programs[END_REF], where a reduction takes a bounded period of time and it is measured by a discrete global clock. Maximal parallel steps are adopted there with a new construct that can e.g. express time-out and pre-emption, and developing suitable temporal variants of bisimilarity might reveal a worthwhile, albeit difficult task.

Definition 7 (

 7 Residuation). Let a, b ∈ A. The residuation of a with respect to b is defined as a ÷ b = {c ∈ A | a ≤ b ⊗ c}. The definition conveys the intuitive meaning of a division operator: indeed, a ≤ b ⊗ (a ÷ b), thanks to distributivity. Also, (a ⊗ b) ÷ b ≤ a and a ÷ (b ⊗ c) = (a ÷ b) ÷ c. Residuation is monotone on the first argument: if a ≤ b then a ÷ c ≤ b ÷ c and a ÷ b = ⊥. For more properties of residuation we refer to [3, Tab. 4.1].

  First, we show that A, c and B, c satisfy the same weak barbs for all c ∈ C. Let (1) and (2) be two fair computations. Since

  ⇓ d and, by the above observation, B, c ⇓ d . Since SCCP is confluent, also γ 2 ⇓ d . The fact that R is closed under -→ * is evident from the definition of R. While for proving that R is upward-closed take γ 1 = A , σ and γ 2 = B , ρ . By Lemma 4 for all a ∈ C, A, c ⊗ a -→ * A , σ ⊗ a and B, c ⊗ a -→ * B , ρ ⊗ a . Thus, by definition of R, ( A , σ ⊗ a , B , ρ ⊗ a ) ∈ R.

α

  --→ A , σ , we need to prove the existence of B and ρ such that B, ρ ⊗ a ⊗ α → B , ρ and ( A , σ , B , ρ ) ∈ R. By Lemma 8 and Lemma 9 we obtain A, σ α ---→ A , σ , and there exists b such that α ⊗ b = a ⊗ α (1) and σ ⊗ b = σ (2). From the labelled transition of A, σ and the hypothesis A, σ ∼ B, ρ , we have that B, ρ ⊗ α → B , ρ , with A, σ ∼ B, ρ (3). By (1) we have B, ρ ⊗ a ⊗ α = B, ρ ⊗ α ⊗ b and B, ρ ⊗ α ⊗ b → B, ρ ⊗ b (due to operational monotonicity). Finally, by the definition of R and (3), we conclude that ( A , σ ⊗ b , B , ρ ⊗ b ) ∈ R, and, by (2), A , σ ⊗ b = A , σ . Theorem 2. ∼ s = ∼ Proof. The equivalence ∼ s =∼ can be proved by using Lemma 10. From ∼ to ∼ sb . We show that R = {( A, σ , B, ρ ) | A, σ ∼ B, ρ } is a saturated bisimulation, i.e., for ( A, σ , B, ρ ) ∈ R the conditions in Def. 15 are satisfied i) If A, σ ↓ c , then we have B, ρ ↓ c by the hypothesis A, σ ∼ B, ρ .

  is a strong bisimulation, i.e., for ( A, σ , B, ρ ) ∈ R the conditions in Def. 17 are satisfied i) If A, σ ↓ c , then we have B, ρ ↓ c by the hypothesis A, σ ∼ sb B, ρ . ii) Suppose that A, σ α -→ A , σ . Then by Lemma 8 we have A, σ ⊗ α → A , σ . Since A, σ ∼ sb B, ρ , then A, σ ⊗ α ∼ sb B, ρ ⊗ α and thus B, ρ ⊗ α → B , ρ with A , σ ∼ sb B , ρ .

Example 1 .

 1 Let us consider the agents ask(c) → stop and stop. To prove that they are weakly bisimilar, it has to be proved that γ ≈ γ for configurations γ = ask(c) → stop, ⊥ and γ = stop, ⊥ . Consider the following relationR = {( ask(c) → stop, ⊥ , stop, ⊥ ), ( stop, c , stop, c )}It is quite easy to prove that it is a bisimulation, and in fact the smallest one identifying the two configurations. It suffices to note that by definition c ÷ ⊥ = c.

S

  = {( ask(c) → stop, d , stop, d ), ( stop, e , stop, e ) | d, e ∈ C ⊗ & c ≤ e}

Table 1 .

 1 Hide Reduction semantics for SCCP.

A symmetric choice A, ⊗, with distributivity with respect to (and thus a⊗⊥ = ⊥) is possible: the monoidal operator would be decreasing, so that for example a ⊗ b ≤ a. Indeed, this is the usual order in the semiring-based approach to soft constraints[START_REF] Bistarelli | Enhancing constraints manipulation in semiring-based formalisms[END_REF].

However, since we consider monoids instead of groups, the set of axiom of diagonal operators is included in the standard one for cylindric algebras.

The set of free variables of an agent is defined in the expected way by structural induction, assuming that f v(tell(c)) = sv(c) and f v(ask(c) → A) = sv(c) ∪ f v(A).

With the usual conventions, so that e.g. (∃ y A)[ y / x ] = ∃ w ((A[ w / y ])[ y / x ]) for w sv(A) ∪ {x, y} and tell(c)[ y / x ] = tell(c[ y / x ]), the latter defined according to Def. 11.

Our rule is reminiscent of (8) in[21, p. 342].

As an example, the law L1 of[START_REF] Saraswat | Semantic foundations of concurrent constraint programming[END_REF] states ask(c) → tell(d) = ask(c) → (tell(c) tell(d)), which is false precisely for the lack of idempotence: c ≤ σ does not imply σ = σ ⊗ c. For the sake of completeness, the other unsound axioms are L10, L11, and L12.

", by the ANR 12IS02001 PACE, and by the Aut. Reg. of Sardinia P.I.A. 2010 "Social Glue".