{'fraction_non_alphanumeric': 0.03761012601762016, 'fraction_numerical': 0.007193041150886584, 'mean_word_length': 4.9346459298477825, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 13, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Tosca: Operationalizing Commitments Over Information Protocols

The notion of commitment is widely studied as a high-level abstraction for modeling multiagent interaction. An important challenge is supporting flexible decentralized enactments of commitment specifications. In this paper, we combine recent advances on specifying commitments and information protocols. Specifically, we contribute Tosca, a technique for automatically synthesizing information protocols from commitment specifications. Our main result is that the synthesized protocols support commitment alignment, which is the idea that agents must make compatible inferences about their commitments despite decentralization.


Introduction
Commitments represent a high-level abstraction for modeling multiagent interaction [Singh, 1999]. The main idea behind commitment protocols is to specify the meanings of messages in terms of commitments [Pitt et al., 2001;Yolum and Singh, 2002]. For example, to capture a purchase, one may specify that a Quote message means creating a commitment from the seller to the buyer to deliver an item in exchange for payment. In addition to meanings, a commitment protocol typically also specifies operational constraints such as message ordering and occurrence. Thus, for example, one would specify that the Quote message cannot occur before the Request For Quote message from the buyer to the seller. Intuitively, the motivation behind operational constraints is to rule out causally invalid protocol enactments.
A fundamental challenge in this line of work has been supporting decentralized enactments of commitment protocols, that is, in shared nothing settings where agents communicate asynchronously. Specifically, the only way for one agent to convey information to another is to send it a message. Supporting decentralized enactments in such settings is nontrivial because agents may observe messages in incompatible orders. Specifically, decentralization may lead to situations where agents deadlock (lack of liveness), observe inconsistent messages (lack of safety), or come to incompatible conclusions about commitments that hold between them (lack of alignment [Chopra and Singh, 2008;Chopra and Singh, 2009;Chopra and Singh, 2015b])-all three properties being crucial to interoperability.
Tosca addresses the challenge of decentralized enactments.
It builds upon the conceptual observation that commitment specification and operational constraints are distinct concerns [Chopra and Singh, 2008;Baldoni et al., 2013]. For simplicity and clarity, from here on, we reserve protocol to mean an operational protocol specifying messages and the operational constraints on their ordering and occurrence. Specifically, the question Tosca answers is: how can we operationalize commitment specifications over protocols such that liveness and safety are preserved, and alignment is guaranteed? Tosca's contribution is a method for automatically synthesizing the appropriate protocol.
Tosca's conceptual contribution is bringing three technical strands on interaction in multiagent systems together. One, BSPL [Singh, 2011], a declarative language for specifying protocols. BSPL protocols are known as information protocols because ordering and occurrence constraints fall out from more fundamental causality and integrity constraints on information in messages. A BSPL protocol can be checked for liveness and safety [Singh, 2012]. Two, Cupid [Chopra and Singh, 2015a], a declarative language for specifying commitments. The semantics of Cupid is in terms of commitment-oriented queries on a relational database. Thus we may imagine an agent that runs (for whatever purpose) commitment-oriented queries on its local database. Three, research on alignment [Chopra and Singh, 2015b] (C&S, for brevity), which is about mechanisms for ensuring that the parties to a commitment (the debtor and creditor) always progress toward states where they make mutually compatible local inferences about the commitment. Specifically, whenever the creditor infers a commitment as active from the messages it has observed, the debtor must as well infer it as active from its own observations. Architecturally, Tosca brings the three strands together in the following manner. Each agent's local database or state comprises the messages it would have sent or received following a BSPL protocol. Cupid enables inferring the states of the commitments an agent is party to from this database. However, because each agent carries out this inference on its own local state, it may turn out that agents are not aligned with respect to a commitment. Tosca gives a method for ensuring progress toward alignment. Specifically, given a BSPL protocol and a set of commitments defined over the messages in the protocol, it gives a method for synthesizing a BSPL protocol whose enactment guarantees progress toward alignment. Furthermore, if the input protocol is live and safe, the synthesized protocol is live and safe as well.
Tosca goes beyond C&S in two ways. One, it addresses alignment for a more expressive language that includes deadlines, nested commitments, and a richer commitment lifecycle. Two, whereas C&S give algorithms for alignment, thereby constraining the implementation of agents, Tosca gives a purely interactive solution in terms of a protocol whose enactment would guarantee alignment.

Background
We now overview BSPL and Cupid, where for clarity we use message (as in BSPL) and commitment (as in Cupid) to mean instances, and specification to mean the respective specifications.

BSPL
BSPL is used to declaratively specify protocols without explicit control flow.
By contrast, languages such as AUML [Huget and Odell, 2004] and RASA [Miller and Mcginnis, 2007] rely on explicitly specifying message ordering. Instead, BSPL protocols impose information causality constraints on each message m: what information m's emission creates and what information the sending role must know before sending m. Thus, an implicit message ordering is imposed based solely on a protocol's explicit and declarative information causality specification.
Listing 1 demonstrates BSPL via the Ordering protocol. From here on, we describe such a protocol as an "input protocol" for Tosca, because it provides general message schemas for taking communicative actions (instantiating messages) and it is distinguished from a synthesized protocol for aligning a commitment.
The protocol Ordering has the roles M (merchant), C (customer), and S (shipper); and the parameters oID (order identifier), item, price, pID (pay identifier), rID (request identifier), and sID (ship identifier).
A complete enactment of Ordering comprises a tuple of bindings for all of its parameters. All parameters are adorned out for the protocol as a whole, meaning that their values are bound by enacting the protocol. Parameter oID is annotated as a key for the other parameters. This means each oID binding corresponds to a distinct tuple of bindings for non key parameters and thus identifies Ordering's enactment. For example, it is not possible for the merchant to send two quotes with key binding oID = 1 and different non key parameter bindings.
Ordering declares four message schemas (their placement is irrelevant). By convention, any key parameter of the protocol is a key parameter for any message in which it appears. The message schema quote on Line 4 is from the merchant to the customer. It has three parameters, whose values are bound by sending a quote due to being adorned out , namely oID, item, and price.
The message schema pay on Line 5 is from the customer to the merchant. It comprises one parameter adorned in , namely oID, which means that its value binding must be known via message emission or reception before a pay message is sent from the customer to the merchant. For example, the customer cannot send a pay message with in parameter binding oID = 1 before receiving a quote message with the same binding. Hence, the customer can only send a pay message after receiving a quote from the merchant with the same key value, based on the information (parameter) causality constraints.
Likewise, the message schema requestShip on Line 6 is from the merchant to the shipper and it has the in parameter oID. Finally, ship on Line 7 has the oID parameter adorned in . Since the shipper can only know about oID 's binding by receiving a requestShip message from the merchant, ship can only be sent after being requested.

Cupid
Cupid is a language for specifying commitments over an event database schema and inferring commitment states based on an event database state. In this paper, we only consider defining commitments over protocol message schemas, where commitments are inferred over messages.
We demonstrate Cupid's basic ideas with an example commitment in Listing 2 defined on top of the message schemas of Listing 1. A Purchase commitment from M (merchant) to C (customer) is created when a quote is made. The created commitment is uniquely identified by quote's key (oID ). Purchase is detached if a payment correlated to a quote occurs within ten time points of the quote (pay and quote both have the same key, oID ). If the payment does not occur by the deadline, then the commitment is expired (failure to meet detach). The commitment is discharged if the (correlated) shipment occurs within five time points of the payment; if the shipment does not happen by the deadline, the commitment is violated (failure to meet discharge). Cupid treats such lifecycle events as first-class events, meaning that one commitment's lifecycle event may depend upon another's.

Separation of Concerns
Architecturally, Tosca uses BSPL to specify the operational layer interaction focusing on informational causality, as a separate concern from the interaction requirements specified in Cupid. For example, we could change Listing 1's requestShip message schema to be causally dependent on pay's identifier (pID ) before emission: The modified information causality does not alter the fact that the Purchase commitment continues to be discharged by a ship message within five time points of the pay message. The modification does alter when these messages can be sent. Conversely, changing the Purchase commitment in Listing 2's discharge from ship to another message would not affect if and when ship can be sent.
Tosca's separation of concerns supports modularity: swapping out a protocol or modifying its information causality does not affect commitment level requirements, only when information (descriptively) can be created and thus when commitments can be met; changing a commitment does not affect if and when information can be created, only the (prescriptive) messaging requirements between parties.

Technical Motivation
We now demonstrate commitment operationalization protocols, which support realizing a commitment's lifecycle and progression towards alignment via messaging. Specifically, given a commitment defined over an input protocol that potentially causes misalignment, we synthesize a commitment alignment protocol as output.
A commitment alignment protocol includes the necessary message schemas for forwarding messages to the creditor and debtor in order to guarantee commitment alignment. Together, an input protocol and multiple commitment alignment protocols are composed to form a commitment operationalization protocol.

Commitments Guaranteed Alignment
The Purchase commitment in Listing 2 is already alignable for the create, detach, discharge, and expired lifecycle events by the input protocol, Ordering, in Listing 1. In Figure 1 (A), at time point 1 after the merchant sends the customer a quote but before the customer receives it, the debtor (merchant) infers that the Purchase commitment is created. Hence the commitment is already aligned (the debtor knows that they are committed) regardless of what the creditor (customer) knows.
When the customer emits pay before time point 2 they infer that the Purchase commitment is detached. Hence, Purchase becomes misaligned, since the creditor (customer) has a stronger expectation of the debtor (merchant) to discharge the commitment, which the debtor does not know. The misalignment is rectified at time point 3, after the merchant receives the pay message.
Subsequently, after the merchant requests the shipper to ship, the shipper sends a ship message to the customer. At time point 4, after receiving the ship message, the creditor (customer) infers that the commitment is discharged and hence does not have a stronger expectation of the debtor (merchant) than what the debtor knows about (alignment).
Alignment for create, detach, discharge, and expired lifecycle events is guaranteed, either because misalignment does not occur (the creditor does not infer stronger expectations of the debtor) or misalignment is rectified via message reception. However, if ship is received after five time points of payment, then the creditor (customer) infers violation whereas the debtor (merchant) cannot (permanent misalignment). Such misalignment requires message forwarding, (e.g., notifying the debtor of ship), which we will cover in the next section.

Commitments Requiring Forwarding
Suppose an escrow service is used instead of direct payment from the customer to the merchant. The EscrowOrdering input protocol in Listing 3 and the EscrowPurchase commitment in Listing 4 capture this situation. In this scenario, we need to introduce a message that forwards another message's occurrence to an otherwise ignorant party. Listing 5 shows a protocol that introduces message forwarding in order to align the EscrowPurchase commitment (Listing 4) for the input protocol, EscrowOrdering in Listing 3. Specifically, by incorporating the message schema, fwdCMPayEscrowID, for forwarding payEscrow from the customer to the merchant. Each forwarding message schema has a distinct name mapped to the message being forwarded.
To exemplify, in Figure 1(B) the customer sends payEscrow to the escrow. At time point 5 we have misalignment, because the customer (creditor) infers the EscrowPurchase's detach and an expectation for the merchant to ship the goods. Yet the debtor (merchant) cannot know the customer's expectation without notification. Misalignment is resolved at time point 6 once the customer forwards payEscrow to the merchant via fwdCMPayEscrow. Both roles know that the debtor (merchant) is expected to discharge the commitment (alignment).

Nested Commitments
We now consider the case where one commitment's lifecycle event depends upon another's (nesting). The EscrowTransfer commitment given in Listing 6 is defined over the message schemas from the input protocol EscrowOrdering in Listing 3. The escrow service is committed to the merchant to transfer the customer's payment, once EscrowPurchase is discharged. EscrowTransfer is operationalized with the protocol in Listing 7. Focusing on the nested lifecycle event, the idea is that if EscrowTransfer's creditor (merchant) infers its detach, then so should the debtor (escrow). EscrowTransfer's detach is EscrowPurchase's discharge. Hence we ensure that whenever a message contributes to EscrowPurchase's discharge it can be forwarded to EscrowTransfer's debtor (escrow). In Figure 2 at time point 7, the merchant infers EscrowPurchase's discharge and consequently EscrowTransfer's detach. Specifically, due to knowing about the messages contributing to EscrowPurchase's discharge: quote (by sending it), payEscrow (via the forwarding message fwdCMPayEscrow), and ship (via the forwarding message fwdSMShip). Yet the debtor (escrow) neither infers EscrowPurchase's discharge nor consequently EscrowTransfer's detach. Hence, the creditor (merchant) expects the debtor (escrow) to discharge Es-crowTransfer, which the debtor is unaware of (misalignment). Forwarding message schemas to the escrow support rectifying the misalignment. EscrowPurchase's discharge is due to: quote, which can be forwarded to the escrow; payEscrow, which the escrow receives (hence no forwarding is required) and ship, which can be forwarded to the escrow. In Figure 1 at time point 8, after sending the forwarding messages, escrow knows about EscrowPurchase's discharge and thus EscrowTransfer's detach (alignment).

Compositionality
Commitment alignment protocols can be synthesized independently and then composed. In Listing 8, our preceding commitment alignment protocols are subprotocols of an overall operationalization protocol. If two commitment alignment protocols bind the same out parameter, it is due to the same message being sent and hence the binding is the same. For example fwdCMPayEscrowID is bound by EscrowPurchaseAl when a forward message fwdCMPayEscrow is sent if and only if fwdCMPayEscrowID is bound with the same value by EscrowTransferAl when the same fwdCMPayEscrow message is sent. Hence, independently constructed alignment protocols are composed together without contradictory parameter bindings during enactment.

Summary
Tosca synthesizes the alignment protocol for a commitment and an input protocol. The alignment protocol comprises forwarding message schemas, supporting participants in aligning the commitment via messaging. Multiple commitment alignment protocols are composed together, without parameter interference, into an operationalization protocol for triggering commitment lifecycles and supporting alignment via messaging.

Protocols
We adopt BSPL's formal syntax from [Singh, 2012]. We use the following lists treated as sets: public roles x, private roles y, public parameters p, key parameters k ⊆ p, in parameters p I ⊆ p, out parameters p O ⊆ p, private parameters q, and parameter bindings v and w. The set of all parameters is p = p I ∪ p O . The in and out parameters are mutually disjoint: p I ∩ p O = / 0. A protocol's references (i.e., subprotocols, including message schemas) are denoted by the set F. Definition 1. A protocol is a tuple P = n, x, y, p, k, q, F where n is a name. x, y, p, q are as above, F is a finite set of f subprotocol references F = {F 1 ,...,F f }, such that P includes each referenced sub protocol F i 's roles, and key and non key parameters (∀i : . An atomic protocol with two roles and no references is a message schema denoted as ⌈s → r : m p( k)⌉.
Later, protocol enactment is defined over a Universe of Discourse (UoD) comprising roles and message schemas (for convenience we modify the original BSPL definition from a UoD comprising message references).
Definition 2. [Singh, 2012, Def. 12] The UoD of protocol P, UoD(P) = R,M consists of P's roles and message schemas including the message schemas of its referenced protocols recursively.

Commitments
A commitment specification is a finite string according to the corresponding representation in Table 1 over a message  schema name set Base. A commitment specification, c(x, y, Cre, Det, Dis) from a debtor x to a creditor y is defined over BSPL protocol message schema references (Base events) used by an input protocol. Role names and time instants are sets R and T , respectively. Operators ⊓, ⊔, and ⊖ are respectively conjunction, disjunction, and exception. In E[l,r], [l,r] is the time interval that E[l,r] occurs within. We omit l and r when they are respectively 0 and ∞.

Commitment Operationalization
Each commitment we wish to operationalize is rewritten into a commitment alignment protocol for an input protocol. A forwarding message schema has a unique name and out parameter, to avoid conflicts with other message schemas.
Let N be the set of unique message forwarding schema names disjoint from the message schema name set Base. Unique forwarding message schema names are obtained taking as input a message schema name from Base and a role, and then outputting a forwarding message schema name, using an assumed injective function V : Base × R → N . For example, fwdSEShip = V (ship, E) is a unique name for forwarding ship from the shipper (S) to the escrow (E). The inverse injective function V −1 determines which message is being forwarded. An assumed injective parameter name function VID : N → ID from forwarding message names to identifier parameter names (ID) produces a uniquely named out parameter for each forwarding message schema (e.g., fwdSEShipID= VID(fwdSEShip)).
A forwarding message schema is included in a commitment operationalization protocol when necessary to support commitment alignment. For example, if E is the commitment's create condition, b the debtor and a the creditor. Then, the event formula E must be aligned between roles a and b such that if a knows E then b can learn of E via message forwarding.
Each commitment C is decomposed via rewrites into instructions of the form al(a, E, b) stating a requirement for E to be aligned from a to b. If the formula E is non atomic, then it is further decomposed to eventually atomic alignment instructions, al(a, m, b) on messages m. Atomic message alignment instructions are rewritten into the necessary message forwarding schema in the alignment protocol that we are constructing. We present the base case rewrites for alignment instructions operating on message schemas, then non atomic event formulae and finally commitments.
The presented rewrite rules are for an input protocol P = n, x, y, p, k, q,F and its Universe of Discourse R,M = UoD(P), a commitment C and the commitment alignment protocol P C = n C , x C , y C , p C , k C , q C ,F C being constructed.
Rule R1 handles aligning an atomic message. It is conditional on: (1) An atomic message alignment instruction al (a,m,b). (2) The commitment alignment protocol P C being constructed. (3) A message schema in the input protocol P where a role s that is distinct from b instantiates the message m via emission to a role r distinct from b.
The rewrite result is: (4) A new message schema labeled m forw acting to forward message schema m's instances, from the role s to the role b. (5) The commitment alignment protocol referencing m forw . (6) The commitment alignment protocol including the forwarding message schema's key parameters, (7) in and out parameters, and roles.
al (a,m,b), Where: • The uniquely named forwarding message schema forwards m to b: m forw =V (m,b). • The forwarding message schema's parameters comprise: keys corresponding to m's (k forw = k); a unique out parameter to ensure that protocol enactment requires forwarding (p forw O = {VID(m forw )}); and in parameters matching m's parameters (p forw I = p), meaning that m must be instantiated prior to it being forwarded.
Instructions to align messages from a to b occurring within a time window are reduced to atomic message alignment instructions. The message that occurs as well as any start or deadline messages are necessarily also aligned from a to b according to the rewrite Rule R4 (omitting cases for time windows without either a start time, a deadline, or both).
al (a,m[s±J,d ±K],b) al (a,m,b) al (a,s,b) al (a,d,b) (R4) To give an example, the EscrowPurchase commitment from the merchant to the customer in Listing 4 is detached when the customer pays the escrow within ten time points of a price quote. Hence we have an alignment instruction al (C,payEscrow[,quote + 10], M) to ensure that when the creditor (customer) knows the detachment so does the debtor (merchant). The alignment instruction is reduced to al (C,payEscrow,M) and al (C,quote,M).
In the input protocol in Listing 3 quote is from the merchant to the customer, guaranteeing alignment, and so al(C, quote, M) is not rewritten. However, payEscrow is not received or sent by the merchant and hence must be forwarded by the customer. The instruction al (C, payEscrow, M) is rewritten to a message schema as in Listing 9.
Listing 9: A partial alignment protocol for the EscrowPurchase commitment in Listing 4 1 E s c r o w P u r c h a s e A l { 2 roles C , M 3 parameters i n oID key , i n pID , o u t fwdCMPayEscrowID 4C → M: fwdCMPayEscrow [ i n oID , i n pID , o u t fwdCMPayEscrowID ] } Both sides of a conjunct are aligned according to Rule R5. Likewise both sides of a disjunct are aligned via Rule R6, since we do not know which runtime messages will occur a priori.
Exceptions are handled by Rule R7. In order to guarantee that when a role a knows L⊖R then so does b, we must ensure that if a knows L then so can b via messaging. Yet, if b knows R then it will never know L ⊖ R to be true, even if a knows L, believes L⊖ R is true and so forwards L to b. Thus we align L from a to b and R from b to a.

al(a,L⊖R,b) al(a,L,b) al(b,R,a) (R7)
For example, a shipment commitment from the shipper to the merchant is discharged if: the item is shipped within five time points of the shipment being requested, except if the shipment is reported as damaged within five time points of being received. Thus we have an alignment instruction from the shipper to the merchant: al (S,ship[,requestShip + 5]  Nested commitment lifecycle events occur when the corresponding lifecycle event for the referenced commitment c(x,y,Cre,Det,Dis) occurs. Hence, we rewrite nested lifecycle events to the conditions under which they occur according to Cupid's semantics with Rules R8 to R12.
al (a,created(x,y,Cre,Det,Dis) al (a,detached(x,y,Cre,Det,Dis) al (a,discharged(x,y,Cre,Det,Dis) al (a,expired(x,y,Cre,Det,Dis) al (a,violated(x,y,Cre,Det,Dis) The final rewrite is for commitments. A commitment is aligned when: if the creditor knows it is created, detached, or violated, then the debtor respectively knows it is created, detached, or violated; and if the debtor knows it is discharged or expired, then the creditor knows it is respectively discharged or expired. Owing to this asymmetry, we rewrite a commitment with Rule R13 to alignment instructions for each lifecycle event.
Definition 3. A protocol P C is a commitment alignment protocol for a commitment C and an input protocol P iff all possible applications of R1 to R13 are made to C, an empty version of P C and P's UoD R,M = UoD(P). Each rule is a monotonic reduction on finite formulae. Hence: Lemma 1. There exists a commitment operationalization protocol P C for each commitment C and input protocol P.
An operationalization protocol is composed from the input protocol and commitment alignment protocols (omitting empty and redundant subprotocols).
Definition 4. Let P = n, x, y, p, k, q,F be an input protocol and C be a set of commitments defined over the message schema names and roles in P's Universe of Discourse R, M = UoD(P). Let each commitment C ∈ C have an alignment protocol P C = n C , x C , y C , p C , k C , q C ,F C for P that includes at least two roles (| x c | ≥ 2). P C = n C , x C , y C , p C , k C , q C ,F C is an operationalization protocol for C and P iff: P C references the input protocol and all commitment operationalization protocols: F C = {n}∪ C∈C {n C }. P C 's roles and key parameters match the input protocol's: x C = x and k C = k. P's out parameters comprise the input protocol's and each commitment alignment protocol's out parameters:

Semantics
In BSPL, each message instance m [s,r, p, v] denotes a sending role s, a recipient r, a parameter vector p with a corresponding parameter binding value vector v. A role's history denotes its sent and received messages in sequence. A history vector comprises each role's history where every received message must have been sent. Definition 5. [Singh, 2012, Def. 5 Singh's [2012, Def. 8] definition). The set of all viable history vectors for a UoD (e.g., a protocol's roles and message schemas) is its Universe of Enactments. Definition 7. Given a UoD R, M , the Universe of Enactments (UoE) for that UoD, U R,M , is the set of viable history vectors [2012, Definition 8], each of which has exactly |R| dimensions and each of whose messages instantiates a schema in M.
In Cupid [Chopra and Singh, 2015a], an agent's model maps from event schemas to event instances, representing the agent's local view of event occurrences. Here, we are dealing with messages and hence a model is simply a role's history albeit substituting each forwarding message with the message it forwards and timestamping each message with the time it became known (via emission, reception, or notification).
Definition 8. Let P be an input protocol and let Base be the message schema names for the message schemas in P's UoD. Let P C be an operationalization protocol for P. A model for a role a's history H and P C is a history M, where each message is in the model m We adopt Cupid's commitment semantics. For brevity, we only define the set of instances for event formula E (e.g., a lifecycle event) entailed by a model M: E M . If E is a non atomic event formula or a lifecycle event, then the result is a database operation on the messages that cause E to occur. For example, the set of all ship instances is denoted as ship . Moreover, the set of tuples modeled by the formulae for shipment occurring within ten time points, ship[0, 10], is returned by selecting all shipment events that occur between zero and ten time points ( ship[0,10] = σ 0≤t<10 ( ship )). A database operation is inductively defined in Cupid for queries corresponding to each event formula type.
Definition 9. Let M be a model and E an event formula. E M is the set of E's instances (a set of tuples combining stored events) returned from the query for E on M according to [Chopra and Singh, 2015a, D 1 −D 20 ].

Properties
An operationalization protocol retains an input protocol's message ordering.
Lemma 2. Let P be an input protocol, and P C be a commitment operationalization protocol. If there is a history vector H in UoD(P)'s UoE then there exists a history vector H C in UoD(P C )'s UoE where for each history H iC in H C the messages instantiating schemas in M are included in the same order of the corresponding history H i in H.
Proof sketch. We include messages from the input protocol's history to the operationalization protocol's corresponding history, if they instantiate a schema in the input protocol. We can always include received messages ([2012, Def. 6]), emitted messages can be included since they do not violate bindings and in parameters are necessarily known by binding parameters in the operationalization protocol's message schemas. Singh [2012] formalizes liveness and safety for BSPL, and gives verification techniques. A protocol is safe iff each history vector in the UoE preserves uniqueness for each binding. A protocol is live iff any enactment can progress to completion such that all parameters are bound.
Theorem 1. Let P C be a commitment operationalization protocol for an input protocol P. If P is safe then P C is safe. If P is live then P C is live.
Proof sketch. Safety: Assume P C is unsafe. Since P C is an operationalization protocol, by Rule R1 (7) it does not introduce out parameters used by another message schema, hence by applying Lemma 2 P must be unsafe as well. Liveness: As for safety, relying on P C not introducing out parameters used by P.
C&S define alignment for active commitments. Definition 10 generalizes it to all states in Cupid's commitment lifecycle. Specifically, if a creditor infers created, detached or violated of a commitment (thereby strengthening the expectation) from its history, then the debtor must as well (i.e., know what is expected of them). Conversely, if a debtor infers discharge or expired (hence weakening the expectation), the creditor must as well. The idea that messages should happen in some time interval relies on a global clock. However, there is the potential for misalignment due to message delays and local clock skews, rather than which messages are emitted and received. Such problems are avoided by making the time intervals an order of magnitude larger than the maximum clock skew and message delays [Cranefield, 2005].
We assume that for a commitment c(x,y,Cre,Det,Dis) being operationalized with respect to a history vector H if when x or y knows a message m and the counter-party receives m they will do so at a time to make the same inferences over Cre, Det, and Dis. Under this assumption, an operationalization protocol is sufficient to support alignment.
Theorem 2 states that a commitment operationalization protocol always makes it possible to rectify alignment via messaging.
Theorem 2. Let P C be a protocol that operationalizes a set of commitments C such that c(x,y,Cre,Det,Dis) ∈ C. If history vector H ∈ U R,M is in P C 's UoE then there exists a longer H ′′ in P C 's UoE that is aligned with respect to c(x,y,Cre,Det,Dis).

Conclusions
Tosca addresses challenges of decentralized commitment enactment. Given a set of commitments defined over a protocol, it enables automatically synthesizing a new protocol that supports alignment, a form of commitment-level interoperability. Furthermore, the synthesized protocol preserves liveness and safety, both of which are also necessary for interoperation. The new protocol may be thought of as a fleshing out of the input protocol. Tosca brings together several advances-in the specification of protocols, commitments, and ideas about interoperability-toward supporting decentralization.
Tosca establishes a separation of concerns between commitments and protocols. Protocols are specified in BSPL whereas commitments are specified in Cupid-languages developed independently of each other. Notably, in Cupid, commitments are defined over a database schema, not a protocol. We use the fact that BSPL specifications are interpreted over databases in layering Cupid specifications over BSPL specifications.
Decentralization is a theme of growing interest, (e.g., for norm compliance [Baldoni et al., 2015] and monitoring [Bulling et al., 2013]). Tosca's architecture is distinct from shared memory (environment) approaches (e.g., [Omicini et al., 2008]). Such approaches would benefit from Tosca in that they would also need a clear specification of interactions, both in terms of meanings and protocols, even if alignment itself would be trivial because of shared memory.
Other works treat commitments [Chesani et al., 2013] and protocols [Yadav et al., 2015] separately without studying their relationship. Günay et al. [Günay et al., 2015] generate commitment specifications from requirements. We understand commitment specifications as requirements and synthesize operational protocol specifications.
Analogously Searle [1995, pp. 26-27] demarcates between constitutive rules, which make social actions possible by ascribing institutional (social) facts, and norms, which prescribe institutional facts. This separation is adopted for commitment protocols overlaying constitutive rules [Baldoni et al., 2013]. Moreover, norms are both defined over institutional facts and interpreted at different levels of abstraction using constitutive rules within agents [Criado et al., 2013] and legal institutions [King, 2016;King et al., 2017]. We separate richer concerns: commitments, focusing on relational information, overlaying operational protocols, focusing on information causality.
Future directions should address limitations and further applications. Tosca maintains agent autonomy, making alignment possible but not regimented and hence limited by the extent to which autonomous agents communicate message notifications. We demonstrated Tosca on a business domain but it could just as well be applied to requirements in other domains that involve interaction. In particular, healthcare and government (e.g., national) contracts, studied in connection with Cupid are prime candidates for Tosca. Since Tosca provides support for messaging requirements via protocols, the extent to which it can be applied to agent development should be investigated (e.g., using communication abstractions supported in agent programming frameworks such as [Boissier et al., 2013]).