Morice Daudi
email: mdaudi@uni-bremen.de

Jannicke Baalsrud Hauge

Klaus-Dieter Thoben

Effects of Decision Synchronization on Trust in Collaborative Networks

Keywords: Trust, collaborative networks, logistics collaboration, decision synchronization, conflicting preferences

In collaborative networks, individual and organizational entities encounter many disagreements over many decisions rights. These disagreements procreate conflicting preferences, which in turn, affect trustworthy amongst partners. To that end, it becomes necessary that partners assume a degree of fairness on decision rights by calibrating positions which they initially consider a final. This calibration involves synchronizing partners' conflicting preferences to a compromise. The objective of this paper, therefore, is to analyze and evaluate the effect of both, compromised and uncompromised preferences on trust. To achieve this, a corresponding behavioral trust model is proposed and evaluated empirically using a logistics collaboration scenario. This evaluation applies a multi-agent systems simulation method. The simulation involves 360 observations with three preferences set as predictor variables. Results show that irrespective of a degree to which conflicting preferences are synchronized, a magnitude of the generated effect on trust, depends as well on other factors like transport cost and extent to which vehicles are loaded. Additionally, if other factors are kept constant, compromised preferences affects trust more positively than uncompromised ones.

Introduction

In today's world, Collaborative Networks (CNs) are increasingly becoming imperative and widely known about the support they provide to resource sharing. Meanwhile, global entities (partners/actors) are also establishing strong social-graphs, intensifying how critical CNs are. As a crucial requisite, partner relationships in CNs rest on a foundation of trustworthiness, particularly, to contexts where partners interact through socio-technical systems. As socio-technical interaction systems provide required support to CNs, they also raise a difficulty on trust management. This difficult, among others, is constituted by a lack of physical cues rich in physical interactions systems. As a consequence, uncertainty about an extent to which partners can uncover presumed consistency in their behavioral patterns becomes a challenge. This consistency relates to a degree of reliability by which partners can confidently rely upon one another. Rendering this confidence through "security primitives of Confidentiality, Integrity, and Availability (CIA) of data or information" [START_REF] Robinson | The Cloud Understanding the Security, Privacy and Trust Challenges[END_REF] appears hard. This hardness originates from various angles, including the least ability of CIA protocols to accommodate partner's behaviors in CNs.

Unlike CIA mechanisms which protect computer-network resources by avoiding malicious agents, CNs emphasize on the confident assurance that partners will behave in a prescribed/expected manner. Fulfillment of this requirement includes investigating partner behaviors in the operational phase of CNs. In the operational phase, while interacting, partners exhibit a range of behaviors, which in turn can generate an effect on collaboration. To that end, understanding partner's behavioral uncertainties and the generated effect on network performance and trust are imperative. As much as various behavioral uncertainties exist in CNs, the present paper concentrates on behavioral uncertainty resulting from negotiation and decision making. In particular, the paper addresses behavioral discontents, which according to [START_REF] Cruijssen | Horizontal cooperation in transport and logistics[END_REF], are set of partners' disagreements over to a particular set of decisions [START_REF] Cruijssen | Horizontal cooperation in transport and logistics[END_REF]. Such disagreements can procreate conflicts, with the higher possibility to affect underlying trustworthy. Such disagreements are described in [START_REF] Okdinawati | A Behavioral Multi-agent Model for Collaborative Transportation Management (CTM)[END_REF] as conflicts concerning partner's perspectives or beliefs. This paper refers to such disagreements as conflicting preferences.

Conflicting preferences on decision rights can affect network performance and underlying trustworthy differently. Context to resulting outcome, the effect can either strengthen or weakens trustworthy. In particular, a partner who enacts preferences to own interests can end up denying welfare of others. Such preference may have a high chance to decrease trustworthy. As a result, rather than remaining centric to own interests, partners urge to assume a degree of fairness in decision rights. Towards this required fairness, synchronizing partners' conflicting preferences is a necessary. While building on this assumption, unsynchronized decisions, according to [START_REF] Simatupang | Supply chain discontent[END_REF], appear in forms of behavioral discontents, namely: rivalry and compromise. These discontents are further described in [START_REF] Simatupang | Supply chain discontent[END_REF] as: (1) rivalry, a partner has high concern to own interests coupled with low concern for others' interests (I win, you lose); (2) compromise, a partner emphasizes on give-and-take bargaining (we both win a bit and lose a bit).

Whereas rivalry decisions can largely impede trust, compromised ones can facilitate its growth and sustainability. Therefore, the present paper investigates the effect of decision synchronization on trust. Alongside this objective, a model depicting behavioral trust has to be established as well. To that end, two research questions are specified: (1) How can behavioral trust be modeled in CN and related domains? (2) How do compromised and uncompromised conflicting preferences affect trust in CN?

The remainder of the paper is organized as follows. Section 2 discusses trust under computational and behavioral perspectives. While section 3 presents research methodology applied by this study, section 4 sheds light on agent preferences and confrontation analysis. In section 5, a behavioral trust model applicable to CNs and related domains, comprising of trust propagation, measurement and assessment is proposed. Section 6 specifies a validation scenario in the domain of logistics collaboration. In section 7, an evaluation consisting of implementation, experiment design, and setup, results and discussions are provided. The paper ends in section 8 by providing conclusion and outlook.

Trust: Computational and Behavioral Perspectives

Trust is generally understood as a degree of confidence agent X develops in agent Y, while believing that Y will behave in ways X expects. Even though, this understanding is made contextual specific depending on application domain and discipline. In psychology, trust is conceptualized a psychological state comprising an intention to accept vulnerabilities [START_REF] Rousseau | Not so different after all: A cross discipline view of trust[END_REF]. In social relational exchanges, trust has a form of reputation aimed to deny betrayal aversion. In economics trust is associated with rational choices against risks aversions. Moreover, in computer science and engineering trust is categorized in groups of "system and user" [START_REF] Sherchan | A Survey of trust in social networks[END_REF]. System trust (hard-trust) addresses relationships among machine nodes, to protect computational systems according to CIA primitives. User trust (soft-trust) concerns a level of confidence trustor-agent has in numerous objects it interact and collaborate with. These objects are like machines, software-agents, humans, and organizations. In essence, user trust is conceived on a behavioral foundation of social, economic, and psychological primitives.

Trust requirements in CNs can largely be founded on social and economic behavioral primitives, with an attempt to reduce uncertainties and resulting vulnerabilities. Adding to these primitives, trust challenges in CNs stem from consortia structure. Structure-wise, CNs consortia are largely dynamic, sometimes engaging actors who are strangers, and configured in the partially seamlessly environment. Within these settings, there can rise a high possibility that partners exhibit behavioral inconsistencies. Such behavioral inconsistencies, can be related but not limited to how: agents share information; divide gains and costs; synchronize, both compatible and incompatible preferences (positions in decision rights); and deviate from goal congruence (opportunism). The present paper, however, concentrates on conflicting (incompatible) preferences.

Research Methodology

Investigation of decision synchronization applies a Multi-Agent Systems (MAS) as the main method, compared to the survey, normal experiments, and case study. On the one hand, the survey appears inappropriate due lack of a process (physical reality) and longitudinal observations. Normal experiments deny social-virtual environments in computational settings while case study might be expensive in terms of resources. On the other hand, relatively, usage of MAS achieves intended purpose. The MAS deploys social structures in computational settings while maximizing process and time under virtual reality.

Therefore, applied methodology follows this sequence. First, an approach to model conflicting preferences, especially those preferences resulting in a mode of conflict is discussed (section 4). Secondly, a model of behavioral trust which integrates CNs life cycle, the definition of trust, and the analogy of human trust propagation is conceived (section 5). To empirically evaluate and validate the model, and also forecast the effect of decision synchronization on trust, the MAS is used. Through MAS, a logistics collaboration scenario is conceived using Agent-Based Modeling (ABM) technique. The collaboration scenario evaluated by using a "PlaSMA Platform" [START_REF] Schuldt | Designing a Simulation Middleware for FIPA Multiagent Systems[END_REF]. PlaSMA is an event-driven simulation system which has been designed to solve and evaluate scenarios of the logistics domain1 .

Agent Preferences: Confrontation Analysis

It is common that agents engage in numerous relationships and dependencies, some of which ending up in dilemmas. Each singleton dilemma involves specific character behavior from participating agents. Highlighted in [START_REF] Murray-Jones | Co-ordinated Positions in a Drama-theoretic Confrontation: Mathematical Foundations for a PO Decision Support System[END_REF], agents face dilemmas at a point when each agent takes a position that it regards as final, called a moment of truth. The positions can be compatible (collaboration mode) or incompatible (conflict mode) [START_REF] Murray-Jones | Co-ordinated Positions in a Drama-theoretic Confrontation: Mathematical Foundations for a PO Decision Support System[END_REF], [START_REF] Bryant | Drama Theory: Dispelling the Myths[END_REF]. If positions are compatible collaboration proceeds. If they are incompatible, agents negotiate by synchronizing (calibrating) positions in their conflicting preferences. Although agents get into negotiation, it is not mandatory that always they end up into a compromise. Works in [START_REF] Murray-Jones | Co-ordinated Positions in a Drama-theoretic Confrontation: Mathematical Foundations for a PO Decision Support System[END_REF], [START_REF] Bryant | Drama Theory: Dispelling the Myths[END_REF], [START_REF] Bennett | Confrontation analysis: prediction, interpretation or diagnosis? In Analyzing Conflict and its Resolution[END_REF] and [START_REF] Hermawan | Holistic Formal Analysis of Dilemmas of Negotiation[END_REF] address six dilemmas, two belonging to collaboration mode and the rest belonging to conflict mode. Collaboration mode is constituted by dilemmas of cooperation and trust; while the conflict mode is constituted by dilemmas of positioning, persuasion, rejection, and threat.

Whereas CNs comprehend on dilemmas of collaboration mode, in some situations, disagreements over the domain of decisions need to be compromised prior advancing to next stage. For example, in a collaboration between shipper and receiver, the shipper may prefer producing in fixed quantities while receiver prefers a production which is consistent with market demand. Such disagreement represents a conflict mode that must be responded to. To any occurring dilemma, according to [START_REF] Bryant | Drama Theory: Dispelling the Myths[END_REF], a character may respond in four ways: (1) by changing its position; (2) by amending its preferences for the possible outcomes; (3) by denying that the dilemmas exist, or; (4) by taking irreversible unilateral action. This study builds on the second and third responses and advances on dilemmas of persuasion and rejection respectively.

Modeling of Behavioral Trust

A proposed behavioral trust model (figure 1) is developed by conceiving an analogy of human trusting process, propagating in three stages: intention, action, and reality. This propagation conforms to a trust building framework in [START_REF] Laeequddin | Trust building in supply chain partners' relationship: an integrated conceptual model[END_REF], generic understandability of trust, and trust definition in [START_REF] Mayer | An integrative model of organizational trust[END_REF]. The human-agent trusting process begins by initiating an intention to trust, that depends on contextual characteristics. Upon satisfying this intention, human-agent engages in action to trust. The action to trust involves establishing an expectation, corresponding to a degree of confidence human-agent develops in an object it desires to trust. The reality is a final stage in which a trust transaction become executed, providing human-agent a feedback through comparing expectation versus an outcome. In particular, the model is conceived by formalizing a dependency between two agents: X a trustor agent, and Y a trustee agent, although this relationship is symmetric. Moreover, as trust can be embedded within trustor or trustee, concordant to [START_REF] Laeequddin | Trust building in supply chain partners' relationship: an integrated conceptual model[END_REF], conception draws on trust embedded within trustee.

{A1, … ,An}

X: Trustor Object

An intention to trust Propensity

Action to trust Expectation (E)

Execution

Reality (S)

Within Above

Trust Assessment

Fig. 1. Behavioral trust model

Under an intention to trust, X initializes its propensity to trust Y. Depending on preferred characteristics and a degree to which are fulfilled, X can commit its propensity to trust. If however, conflicting preferences arise, X and Y negotiate seeking a compromise. On passing the intention to trust, X propagates to an action to trust. In this stage, X utilizes existing factual data from Y to develop a degree to which it can trust Y (expectation). This expectation forms a level of confidence, assurance or reliability which X develops in Y. Alongside its decision, X can: [START_REF] Robinson | The Cloud Understanding the Security, Privacy and Trust Challenges[END_REF] accept being vulnerable to Y's actions, or; (2) withdraw its action to trust if the payoff is perceived unsatisfactory. If X accepts vulnerabilities, for each underlying performance indicator, it specifies its range of expectation. Upon proceeding to reality stage, X loses control in hands of Y (during execution). Hereby, a transaction is executed and resulting outcome observed. Afterward, X measures trust (effect) by comparing resulting outcome to expectation it developed. In measuring and assessing trust, a specific level of trust is determined to depend on trust meter. For example, on applying a three scale meter, the outcome can be below, within, or above expectation.

Logistics Collaboration: A Validation Scenario

Validation of the behavioral trust model employs a collaboration scenario in logistics. The scenario is preceded by requirements definition as well as conceiving agents' interactive negotiations.

Collaboration Requirements

Logistics collaboration, among others, seeks to increase asset utilization, reduce costs, and improve customer services and efficiency. While exploiting these goals, confrontational preferences concerning issues like production, distribution and demand of goods can affect underlying trustworthy. As long as such preferences remain uncompromised, they threaten collaboration future, leading to the uncertain and vulnerable outcome. Although many preferences affect trust in logistics collaboration [START_REF] Daudi | A Trust Framework for Agents' Interactions in Collaborative Logistics[END_REF], this study concentrates on three preferences (Table 1); where shipper, carrier and receiver are collaborating agents. Shipper represents manufacturers, suppliers, sellers and individuals. Carrier agent represents transporters, moving goods to receivers. Receiver agent represents retailers, distributors, buyers, and end consumers. The three preferences are described as follows. Shipper prefers producing goods in fixed quantities (P1). Equally, carrier perceives delivering goods in fixed quantities (P2), and; full truck (P3). Each preference has a threatened future (conflict) to be synchronized to a compromise or rejection.

Agents' Interactions and Negotiations

Agent-Based Modeling (ABM) is applied to model, understand and prognosticate behavioral effect resulting from agents' decision synchronization in logistics collaboration. The ABM method is preferred because of its ability to capture emergent phenomena, and provide a natural description of a system [START_REF] Bonabeau | Agent-based modeling: Methods and techniques for simulating human systems[END_REF]. Correspondingly, building on both, weak and strong agent notions as discerned in [START_REF] Wooldridge | Intelligent agents: Theory and Practice[END_REF], collaborating agents are conceived autonomous, reactive, adaptive, with the ability to act socially. This implies, shipper, carrier, and receiver are limited to information related to planning and forecast of production, carriage and demand. As such they learn from previous experience, trying to match similar prospects. Moreover, each agent possesses objectives together with possible constraints. Among the constraints are conflicting preferences (Table 1). As such, shipper focuses on minimizing backorders and inventory, receiver focuses on increasing saving on transportation costs, and carrier seeks to maximize full truck.

Fig. 2. Generic behavioral descriptions of agents in logistics collaboration

While the behavioral description of the collaboration scenario (figure 2) draws from previous work in [START_REF] Daudi | A Trust Framework for Agents' Interactions in Collaborative Logistics[END_REF], its respective modeling proceeds as follows. A brokeragent invites shippers, carriers, and receivers (participants) by issuing a Call For Proposal (CFP). In its CFP, broker-agent set required specificity, including an estimated number of pallets to be produced and demanded/consumed, and required carriage capacity. Upon receiving CFP, each participant performs own internal assessment on its capability to fulfill CFP requirements. Afterward, each participant replies to broker-agent by proposing or reject the CFP. If rejected, the CFP is brought to an end. If proposed, each participant sends a proposal reply to broker-agent. In turn, broker-agent assess the proposal against established specificity. Depending on assessment outcome (satisfactory specificity), broker-agent either accepts, adjusts or rejects the proposal. If found satisfactory, broker-agent engage participants in forecasting their orders, compromise conflicting preferences as well as developing expectations. Finally, during the execution of orders, goods are moved by the carrier from shipper to receiver. Along this execution, actions of each participant are observed subsequent to recording actual score (reality).

Specific to conflicting preferences, during negotiation, for each preference an agent takes a position that may differ to that of others, resulting in disagreements. These disagreements lead to a threatened future of a specific preference. To compromise disagreements, three alternatives exist acceptance, persuasion, and rejection. The acceptance alternative occurs if rival agents see that the threatened future is attractive. In this case, the preference changes to collaboration mode of a dilemma (cooperation or trust), thus, disqualified to constitute disagreements. If however the threatened future is unaccepted, the respective agent engages in persuading other agents to its position or reject the existence of the threat. The persuasion of the threatened future goes along with a provision of incentives to rivals, together with a promise that the agent whose future is threatened will act trustworthily (Table 2). Finally, if a threat is rejected, collaboration proceeds with a condition that associated vulnerabilities, if they occur, will bear a penalty to the agent which rejected the existence of that threat. Table 2 summarizes exemplified incentives as well as award and penalty to a persuaded and rejected preference.

Evaluation

This section details an assessment of applicability, usefulness and conceptual validity of the behavioral trust model. Secondly, it examines effect, compromised and uncompromised conflicting preferences generate on trust. Accordingly, details of implementation (sub-section 7.1), experiment design and setup (sub-section 7.2), experiment results (sub-section 7.3), and discussions (sub-section 7.4) are presented.

Implementation

A simulation prototype is set a centralized network configured and managed by a neutral trustee (broker). It comprises of 2 carriers, 6 shippers, and 6 receivers. All agents including the broker, exchange messages structured according to FIPA standards [17] using logistics collaboration ontology. The protocol type of negotiation is adapted from [START_REF] Berndt | Anticipatory Behavior of Software Agents in Self-Organizing Negotiations[END_REF], such that owner of a preference whose future is threatened has to propose a persuasion which can either be accepted or rejected. Furthermore, all participating agents, upon being initialized, they register in a directory facilitator named as "collaboration", that provides yellow page services. Collaboration begins only when it is activated by the broker agent. The broker agent monitors collaboration by managing parameters exchanged, and it measures and evaluates trust levels.

Experiment Design and Setup

To examine the effect of decision synchronization on trust, MAS simulation experiment is designed as follows. Three predictor variables (P1, P2, and P3), with each predictor having two levels (Persuasion, Rejection) are designed to affect response variables. The experiment employs two response variables: transportation cost and full truck. The response variables are used to determine the internal-oriented performance of logistics collaboration, and subsequently, the trust level. Moreover, while each experiment yields 6 observations, the same experiment is replicated 6 times to estimate experimental errors. Thus, 10 experiments are conducted, leading to 360 (6 x 6 x 10) observations. The experiment setup involves three events, three experimental unit, generation of random numbers, as well as distinct approaches to verify the model. The events comprise changes in collaboration lifecycle: from planning to forecast, and finally to operation. The planning, forecast, and operation stages correspond to periods of one month, one week, and six days respectively. In view of experimental units, the setup employs shipper, carrier, and receiver. Additionally, various techniques including the use of trace and checking of simulation outputs for their reasonableness are applied to verify behavioral trust model. As the simulation uses randomly generated data, a care is taken on seed generation to assure that generated numbers do not affect final conclusion. To fulfill this requirement, linear-congruential generators are used. Furthermore, to verify that generated numbers are uniformly distributed, generated numbers are scrutinized by chi-square test. Uniquely, each predictor level is assigned own seed value to avoid wrong correlation. Finally, a confidence interval statistical technique is applied to determine conceptual validity of the behavioral trust model.

Experiment Results

Results obtained by conducting MAS simulation experiments are summarized in Table 3. In these results, preferences were combined in a form or code of ABC by using notations "P" and "R". Notations P and R denoted a persuaded and rejected preferences respectively. Similarly, the ABC combination corresponded to preferences P1, P2, and P3 respectively. As an illustration, a combination PPR means shipper's preference (P1) was persuaded, carrier's preference (P2) was persuaded, while carrier's preference (P3) was rejected. Measurement and assessment of trust level applied parameters of cost saving and full truck. In particular, cost saving (reduction in transport costs) was benchmarked to a 15% per pallet as remarked in [START_REF] Tseng | Position Paper on Compensation Rules. Collaboration Concepts for Co-modality[END_REF]. Equally, an extent to which a truck is filled was benchmarked to a 95% as remarked in [START_REF]Collaborative Transportation Management White Paper, Version 1.0. CTM sub-committee of the voluntary inter-industry commerce standards[END_REF]. That is, a truck is considered full if it is loaded to over 95% of its capacity. Following these benchmarks, transportation cost and full truck were operationalized as follows. That, agent, develops an expectation of 15 % of cost saving on transportation cost and a 95% of a full truck. Upon comparing these expectations and corresponding scores, one among the following outcomes occurred: (1) less than expectation, which implied "less trustworthy" with a trust level of 1; (2) very close to expectation, which implied "trustworthy" with a trust level of 2, and; (3) above the expectation, which implied "more trustworthy" with a trust level of 3. In addition, since there were two performance criteria (cost saving and full truck), corresponding trust levels were aggregated by using the mean average. Due to this aggregation, some results generated a trust level of 2.5 and were marked with an asterisk (*) (Table 3).

Alongside these results, and on top of verification approaches used, the study achieves a 95% accuracy in determining model's validity as well as generated results (Table 4). Additionally, overall mean trust level of 1.890 is observed.

Discussions

This research has focused on designing a behavioral trust model, and determine how compromised and uncompromised conflicting preferences affect trust. Concerning modeling of behavioral trust, the analysis indicates that confidence intervals overlap considerably to an extent that mean of each experiment falls in the intervals of others.

In addition, the confidence intervals are within the overall mean trust level. At an accuracy of 95%, it is established that there is no significant variation in results generated by the model. To that effect, theories and assumptions underlying the behavioral trust model, as well as its reasonableness are correctly valid. Concerning how decision synchronization affects trust, the following are deduced. On the one hand, whether a preference is persuaded or rejected, its effect on trust depends as well on other existing factors. Reflecting on logistics and collaboration scenario, synchronized preferences are dependent on an extent to which the truck is filled. Taking serial numbers 3 versus 11 (Table 3) for example, preference combinations PRR affects trust in different magnitudes. Similar cases are also noted in serial numbers 7 versus 14; 6 versus 19; 2 versus 10 versus 16, and; 8 versus 21. In particular, more trustworthy is experienced in cases where both carriers' preferences are persuaded and the truck is at least filled to its full capacity. In such cases, shippers and receivers benefit lowered transportation cost by 20% (Table 2), thus realizing a potential relief. On the other hand, if the full truck condition is held fixed, persuaded preferences generate better trust level compared to those in which preferences are rejected. This is observed in serial numbers 14 versus 21 as well as 9 versus 21.

The findings of this research have a number of crucial implications for practice. On the foremost, irrespective of the degree to which preferences are synchronized, a magnitude of the generated effect on trust is dependent on other contexts, if any. This dependence, however, is unlikely a guarantee to a partner who chooses to reject an existence of the threatened future. It has been demonstrated that other contexts (factors) can be in a position to favor or oppose the ignored threat future. Furthermore, under similar conditional settings, persuaded preferences are better than rejected ones (serial numbers 7 versus (8 and 21)). Finally, as collaboration seeks to compromise conflicts and build a foundation of trustworthy, it is prominent to persuade conflicting preferences than rejecting their existence. Remarking on a second research question, in the overall, compromised preferences in decision rights appear to be a better strategy than uncompromised ones.

Conclusion and Outlook

This paper addresses behavioral discontents resulting from disagreements collaborating partners encounter in decision rights. According to confrontational analysis, such disagreements occur when "each partner takes a position that it regards as final, called a moment of truth" [START_REF] Murray-Jones | Co-ordinated Positions in a Drama-theoretic Confrontation: Mathematical Foundations for a PO Decision Support System[END_REF]. Such disagreements are referred to as conflicting preferences. Appearing in the form of rivalry decisions, conflicting preferences affect trustworthy, especially when partners are denied of assumed fairness. This paper concentrates on investigating an extent to which synchronized and unsynchronized conflicting preferences affect trustworthy. In its first place, the paper contributes by devising a generic model that describes behavioral trust in CNs. Subsequently, the behavioral trust model is evaluated empirically using MAS method in logistics collaboration scenario.

In particular, a generic model of behavioral trust can be applied to CNs other than logistics in the operational phase. Concerning results presented in this paper, two critical insights are revealed. Firstly, synchronized preferences affect trust positively than unsynchronized ones. Secondly, irrespective of a degree to which conflicting preferences are synchronized, a magnitude of the generated effect on trust, depends as well on other factors. Future works will involve investigating a larger set of conflicting preferences in a combined form as well as effect generated by other collaborative processes, like incentive alignment and opportunism.

Table 1 :

 1 A matrix of conflicting preferences and threatened future (adapted from[START_REF] Okdinawati | A Behavioral Multi-agent Model for Collaborative Transportation Management (CTM)[END_REF])

	Agent		Positions		Threatened future
	options	Shipper	Receiver	Carrier
	Shipper -P1 Fixed production	Consistent with	Both options	Fixed production
		quantities	demand		quantities
	Carrier -P2 Consistent with	Consistent with	Fixed delivery	Fixed	delivery
		demand	demand	quantities	quantities
	Carrier -P3 Both options	Both options	Full truck	Full truck

Table 2 :

 2 A matrix of preferences, award and penalty

	Preference	Persuasion	Rejection
	P1	Pay receiver 10% per pallet in case of	Charge 10% per pallet as storage
		backorder, and promise to be trustworthy	cost in case of inventory
	P2	Lower transportation cost by 10 % per	Charge extra 10% of transportation
		pallet, and promise to be trustworthy	cost per pallet
	P3	Lower transportation cost by 10 % per	Charge extra 10% of transportation
		pallet, and promise to be trustworthy	cost per pallet

Table 3 :

 3 A summary of results on synchronized preferences on performance and trust level

	S/N Combined	Frequency Cost Saving	Full Truck	Trust Level
		Preferences
	1	PPR	23	Less than 15% Less than 95% Less trustworthy
	2	PRP	12	Less than 15% Less than 95% Less trustworthy
	3	PRR	8	Less than 15% Less than 95% Less trustworthy
	4	RPP	27	Less than 15% Less than 95% Less trustworthy
	5	RPR	19	Less than 15% Less than 95% Less trustworthy
	6	RRP	16	Less than 15% Less than 95% Less trustworthy
	7	RRR	30	Less than 15% Less than 95% Less trustworthy
	8	PPP	14	Above 15%	Less than 95% Trustworthy
	9	PPR	1	Within 15%	Above 95%	Trustworthy*
	10	PRP	1	Within 15%	Above 95%	Trustworthy*
	11	PRR	15	Less than 15% Above 95%	Trustworthy
	12	RPP	15	Above 15%	Less than 95% Trustworthy
	13	RPR	2	Within 15%	Within 95%	Trustworthy
	14	RRR	36	Less than 15% Above 95%	Trustworthy
	15	PPR	18	Within 15%	Above 95%	Trustworthy*
	16	PRP	17	Above 15%	Above 95%	More trustworthy
	17	RPP	2	Within 15%	Above 95%	Trustworthy*
	18	RPR	30	Within 15%	Above 95%	Trustworthy*
	19	RRP	22	Within 15%	Above 95%	Trustworthy*
	20	RPP	32	Above 15%	Above 95%	More trustworthy
	21	PPP	20	Above 15%	Above 95%	More trustworthy
	Less trustworthy = 1; Trustworthy = 2; Trustworthy* = 2.5; More trustworthy = 3

Table 4 :

 4 A 95% CI for 36 observations in each experiment Exp. 1 Exp. 2 Exp. 3 Exp. 4 Exp. 5 Exp. 6 Exp. 7 Exp. 8 Exp. 9 Exp. 10

	Lower 1.46	1.70	1.60	1.47	1.52	1.90	1.79	1.73	1.75	1.58
	Upper 1.96	2.14	2.18	1.90	1.98	2.32	2.29	2.24	2.22	2.09

http://plasma.informatik.uni-bremen.de/


Introduction

In this work, we present a method for verifying safety properties on Lustre [START_REF] Halbwachs | The synchronous data ow programming language lustre[END_REF] programs. The method consists of a translation of the Lustre programs into a popular representation used in program verication: Horn clauses with constraints. Dierent prover tools (Z3Prover [START_REF]Z3 Theorem Prover[END_REF], Vaphor [START_REF] Monniaux | Cell morphing: from array programs to array-free Horn clauses[END_REF]) are used to reason on the generated formula. Considering the improvements made on prover tools, we expect that they will successfully argument about the majority of the formulas generated from reduced complexity Lustre programs.

In Section 2 a brief introduction on the Lustre programming language and Horn clauses is given. Section 3 describes the contribution of our work, presenting the denitions of translating Lustre code into Horn clauses. Section 4 begins by briey presenting the implementation details, continued by a discussion on the obtained experimental results. Section 5 concludes the report with the current limitations and future improvements that could be made.

Background

Basics of Lustre

Lustre [START_REF] Halbwachs | The synchronous data ow programming language lustre[END_REF] is a synchronous data ow programming language introduced by researchers at Verimag [START_REF]Verimag Research Center[END_REF] in 1984. It is dedicated to the programming of reactive systems, particularly used in critical applications (power plants, airplanes, etc.). It is a data ow (every variable or expression denotes a sequence of values) and synchronous (programs are ruled by a clock) declarative programming language [START_REF] Morel | Ecient compilation of array iterators for lustre[END_REF].

As presented in [START_REF] Benveniste | The synchronous languages 12 years later[END_REF], in Lustre every variable or expression denotes a ow, i.e., a possibly innite sequence of values of a given type. Conceptually, we can think about a Lustre program as an innite loop, where each variable and expression takes their n th value of its sequence at the n th step in the loop. All usual arithmetic (+,-,*,/,div,mod), boolean (or,and,not), relational (=, <>, <, <=, >, >=) and conditional (if..then..else..) operators are provided.

RT n°0492

There are two additional temporal operators, which provide the essential descriptive power of the language:

the pre operator is used to talk about a value of a ow from the previous step. So, if X represents the sequence X = (x 0 , x 1 , .., x i , x i+1 , ..), then pre(X) = (nil, x 0 , x 1 , .., x i-1 , x i , ..).

the → (followed by) operator was introduced to deal with the nil value from the head of the pre(X) sequence. So, Y = 0 → pre(X) denotes the sequence of (0, x 0 , x 1 , .., x i , ..).

We dene variables using equations : on the left having the variable which is dened by the expression on the right. Using pre operator recursive denitions of a variable may be provided.

Lustre programs are structured into nodes. A node is a system of equations having inputs, node cpt(reset:bool) returns (sevseg: int; led_on: bool) ; let sevseg = 0 -> if (reset or pre(sevseg = 9)) then 0 else pre(sevseg)+1; led_on = true -> if reset then pre(led_on) else not(pre(led_on)) ; tel Now, we present the syntax of a subset of Lustre used in this work, eliminating some of the advanced options of writing a Lustre program. We consider that a node has the following skeleton: node node_name(in1_name:type;in2_name:type;..) returns (out1_name:type;out2_name:type;..);

[local variable declarations] let {equations} tel A Lustre variable can be dened having the following type, user-dened data types being unsupported for the moment: In the above denition, var can be one of the previously dened datatypes and op is one supported operator of the associated data type. For further information about the supported operations, the Lustre V6 Reference Manual [START_REF] Jahier | The Lustre V6 Reference Manual[END_REF] can be consulted. Of course, in a real program there are complex equations including several previously presented denitions, but we can always perform a split and transform them to t the presented grammar.

Array iterators One of the main novelties in Lustre-V6 is to provide a notion of higher-order programming by dening array iterators to operate over arrays. In the following, the 5 ve array iterators are presented (as in Lustre-V6 Reference Manual [START_REF] Jahier | The Lustre V6 Reference Manual[END_REF]). In Figure 2, a graphical interpretation of the iterators is presented.

The map iterator transforms a scalar-to-scalar node/operator into an array-to-array node/operator.

Example 1. map <<

+; 3 >> ([1, 0, 2], [3, 6, -1]) [4, 6, 1]
The red iterator transforms a scalar-to-scalar node/operator into an array-to-scalar node/operator. The node argument must have a single output, a rst input of the same type, and at least another input.

Example 2. red << +; 3 >> (0, [1, 2, 3]) 6

The ll iterator transforms a scalar-to-scalar node/operator into a scalar-to-array node/-

RT n°0492

The llred iterator generalizes the ll and the red ones. It maps a scalar-to-scalar node into a scalar and array to scalar and array node. The node argument must have a (rst) input and a (rst) output of the same type, and at least one more input and one more output. The degenerated case with no other input (resp. output) corresponds to the ll (resp. red) iterators.

Example 4. A classical example is the binary adder, obtained by mapping the full-adder.

The unsigned sum Z of two bytes X and Y, and the corresponding overow ag can be obtained by: (over, Z) = f illred << f ulladd, 8 >> (f alse, X, Y ), where: node fulladd(cin, x, y : bool) returns (cout, z : bool); 2 let z = cin xor x xor y; 4 cout = if cin then x or y else x and y; tel

The boolred iterator has 3 integer static input arguments: boolred << i; j; k >> such that 0 ≤ i ≤ j ≤ k and k > 0. It denotes a combinational node whose prole is bool ∧ k → bool, and whose semantics is given by: the output is true if and only if at least i and at most j elements are true in the input array.

Example 5. Two basic boolean array operations:

(a 1 , .., a n ) boolred << 0, 1, n >> (a 1 , .., a n ) nor(a 1 , .., a n ) boolred << 0, 0, n >> (a 1 , .., a n )

Inria

Example 6. Let us consider as an example the Lustre node graphically presented in Figure 1.

Suppose, we want to add an observer, to monitor the value of sevseg variable, which should always remain between 0 and 9. To do this, the following observer node is added in the same program where the node cpt is dened.

node obs(o_reset:bool) returns(ok:bool); var o_sevseg:int; o_led_on:bool; let o_sevseg,o_led_on = cpt(o_reset); ok = o_sevseg >= 0 and o_sevseg <= 9; tel for now, let us not to use the semantics of Lustre and just consider a simple nite state automaton as presented in Figure 3. From state start without any modication, the system evolves to state init, where the rst element of an array a is set to 42 and an index, n, is initialized. From state init the system evolves into a loop-like state, inc, where the rest of the array elements are initialized.

For each state from the automaton we consider a state predicate in Horn encoding with all variables used in the system, i.e., a,n.

init (a, n) =⇒ state inc (a, n) ∧ a[0] = 42 ∧ n = 1 ∀a, ∀n : state inc (a, n) ∧ n < 20 =⇒ state inc (a, n ) ∧ a[n] = n ∧ n = n + 1 ∀a, ∀n : state inc (a, n) ∧ n = 20 =⇒
arity = N input_vars + N output_vars + N local_vars + 1, (1)
i.e. the number of all variables + 1 (time-stamp counter -t, representing the t th step of execution).

We think about Lustre variables as an innite sequence of values: when translating into Horn encoding, a simple Lustre variable becomes a unidimensional array of the same type. In Horn encoding, to show that we are dealing with an array, the following notation was adapted: a simple Lustre variable x, in Horn encoding becomes a x . Similarly, a unidimensional array variable in Lustre will be translated as a 2-D array into Horn encoding.

Modeling the program ow In a Lustre program, the →(followed by) and pre operators are frequently used in order to use the value of a variable from previous step. The use of these operators rise the problem of variable initialization. In order to resolve the conicts related to this problem, just as in case of state automaton, a starting state needs to be generated, with the time-stamp t = 0, meaning that the execution has not started yet, but when it starts, this is the place from where the rst step should be generated:

∀a in , ∀a cond , ∀a x , ∀t : true =⇒ start(a in , a cond , a x , 0)
In case of the →(followed by) operator, with the above predicate being true, the state predicate of the rst step will be generated, containing the initial value of the output variables. It is important to mention, that the current output, will never be observable in the state in which it is set, only in the following one: so the rst output, a x [0], is observable for the rst time in: state x (a in , a cond , a x , 1).

(

) 2
If the state predicate (2) has been generated in a clause, we say that state x is valid at t = 1.

Similarly, when we generate the translation of an arbitrary expression, we have to make sure that all the variables that appear in the right-side of the expression have their state predicates valid at moment (t + 1), so we can access the array element at index t. This ow of variable Inria initialization is illustrated in Figure 4. Note that if the right-side of the expression contains only input variables, there is no need for variable validation. As they come from an external source, not being generated during the execution of the program, they are considered to be valid in every moment of the execution. Expressions Now, we propose an encoding of all variable denitions following a classical syntax directed translation. As an example, we consider a Lustre node with 2 input variables(in, cond ) and one output variable: x, the total arity of a state predicate being 4. Respecting the previously mentioned consideration that in Horn encoding we associate one state predicate for each output and local variable, in the following denitions we will have one state predicate: state x . Inputs are considered to be valid from the start of execution, so there is no need of making validations about them. Each equation below is, implicitely preceeded by ∀a in , ∀a cond , ∀a x , ∀t:

x ::= var is translated with:

(t ≥ 0) =⇒ state x (a in , a cond , a x , t + 1) ∧ a x [t] = var,
where var may be an input, a literal or a temporary denition of a numerical expression. In this last case, we have to make sure that the value of var is valid in the corresponding moment. The previous translation becomes:

(t ≥ 0) ∧ state var (a var , t + 1) =⇒ state x (a in , a cond , a x , t + 1) ∧ a x [t] = a var [t],
x ::= var 1 op var 2 is translated with:

(t ≥ 0) =⇒ state x (a in , a cond , a x , t + 1) ∧ a x [t] = a var1 [t] op a var2 [t],
where op is an operation, supported by the type of x, and var 1 ,var 2 are the operands (may be inputs, constant values, temporary denition of another numerical expressions). In the last case corresponding state validations should be made. If var 1 is missing we are dealing with an unary operation.

x ::= var 1 → var 2 is translated with:

(t = 0) ∧ start(a in , a cond , a x , t) ∧ state var1 (a var1 , t + 1) =⇒ state x (a in , a cond , a x , t + 1) ∧ a x [t] = a var1 [t] (t > 0) ∧ state var2 (a var2 , t + 1) =⇒ state x (a in , a cond , a x , t + 1) ∧ a x [t] = a var2 [t] x ::= pre(var) is translated with: RT n°0492 (t >= 0) ∧ state var (a var , t) =⇒ state x (a in , a cond , a x , t + 1) ∧ a x [t] = a var [t -1]
x ::= ite(bool_var, var 1 , var 2 ) has the following associated clause:

(t ≥ 0) ∧ state bool_var (a in , a bool_var , a x , t + 1) ∧ state var1 (a var1 , t + 1) ∧ state var2 (a var2 , t + 1) =⇒ state x (a in , a bool_var , a x , t + 1) ∧ a x [t] = ite(a bool_var [t], a var1 [t], a var2 [t])
Example 7. Using the above denitions, the translation of the following Lustre node is:

node inc() returns (x:int); let x = 0 -> pre(x)+1; tel

∀a x , ∀t : true =⇒ start(a x , 0) ∀a x , ∀t : t = 0 ∧ start(a x , t) =⇒ state x (a x , t + 1) ∧ a x [t] = 0 ∀a x , ∀t : t > 0 ∧ state x (a x , t) =⇒ state x (a x , t + 1) ∧ a x [t] = a x [t -1] + 1
Connecting multiple nodes Usually, a Lustre program is constructed from multiple user dened interconnected nodes. From a main node, several secondary nodes may be called in order to obtain a partial result, then computing the output of the main node using the partial results from secondary nodes. One representative example, adapted after the example from [START_REF] Jahier | The Lustre V6 Reference Manual[END_REF], is the detection of falling edges in a stream of boolean inputs: to obtain a node, which is detecting falling edges, a node detecting rising edges may be dened; calling this node, with the negated inputs the falling edge detector node can be obtained. As one may observe, in order to make a call for an another node, we have to provide the correct inputs(parameters of the node call) and specify the variable(s) where the result(s) should be stored(left-side of the expression). We are not interested in accessing the local variables of the called node.

Having the above considerations we extend the our Horn clause translation model with a new type of predicate: let us call it interface predicate. Every node used in a Lustre program, should have an interface predicate, which arity may dier from the usual state predicate, because of leaving out the local declarations. An interface predicate consists of the nodes' inputs and it's outputs for every time-stamp, t >= 0. When should the interface predicate be validated? At the moment when all the outputs of the node are valid for the current step.

Let us consider the following Lustre node header with 2 inputs, 1 output and 1 local variable: Inria node do_work(m,n:int) returns (x:int); var s:int;

The Horn clause which generates the interface of the node can be dened as follows:

t ≥ 0 ∧ state x (a m , a n , a x , a s , t + 1) =⇒ interf ace do_work (a m , a n , a x , t + 1)
Whenever, in the calling node an expression appears which calls the second node, when generating the translation, we have to make sure that the called node's interface is valid at timestamp t + 1, with the correct inputs: so we can simply match the outputs of the called node, with the variables from the calling node.

Note that, if the parameters of the called node are computed in the calling node, we also have to make sure that their value is valid in the moment of calling the interface. The Horn clause generated from translating a node call expression (z = do_work(c, d)) is:

t ≥ 0 ∧ interf ace do_work (c, d, z, t + 1) =⇒ state z (c, d, z, .., t + 1)
Note that in this case, we do not have to store anything, because the element is already dened in the called node, and the output of the called node is matched with the variable from the calling node.

Observer nodes Remember that in Section 2 we introduced observer nodes in order to express safety properties on programs. We execute the following steps to make program verications: we consider a node, let us name it obs, as being the main node of the program. The node has a single boolean output, ok, representing the property which needs to be satised. from the obs main node a call is made to the node of the program which computes the result which follows to be veried. having the value of the result from the node call, the ok is computed applying the wanted property on the result. the last step is to generate the Horn clause, which implies that ok is true in every moment: ∀t, ∀a ok : state ok (a ok , t + 1) =⇒ a ok x = 0 -> var_2; tel

The Horn clause translation of this new node is (the universal quantier declarations from now on will be omitted):

RT n°0492 true =⇒ start(a x , a var1 , a var2 , 0) t ≥ 0 ∧ state x (a x , a var1 , a var2 , t) =⇒ state var1 (a num , a x , a var1 , a var2 , t + 1) ∧ a var1 [t] = a x [t -1] t ≥ 0 ∧ state var1 (a x , a var1 , a var2 , t + 1) =⇒ state var2 (a x , a var1 , a var2 , t + 1) ∧ a var2 [t] = a var1 + 1 t = 0 ∧ start(a x , a var1 , a var2 , t) =⇒ state x (a x , a var1 , a var2 , t + 1) ∧ a x [t] = 0 t > 0 ∧ state var2 (a x , a var1 , a var2 , t + 1) =⇒ state x (a x , a var1 , a var2 , t + 1) ∧ a x [t] = a var2 [t]
The interface of the node:

t ≥ 0 ∧ state x (a x , a var1 , a var2 , t + 1) =⇒ interf ace inc (a x , t + 1)
We want to verify a safety property on this program: the output of the node always stays positive, i.e. x >= 0. In the same le we declare an observer node. From there a call is made to the node inc storing it's result into an auxiliary variable aux. Then we compute the output of the observer node, with the equation: ok = aux >= 0, i.e. the property we want to verify.

The Lustre description of the observer node: node obs() returns(ok:bool); var aux:int; let aux = inc(); ok = aux >= 0; tel The observer node is translated into Horn encoding t ≥ 0 ∧ interf ace inc (a aux , t + 1) =⇒ state aux (a ok , a aux , t + 1) t ≥ 0 ∧ state aux (a ok , a aux , t + 1) =⇒ state ok (a ok , a aux , t + 1) ∧ a ok [t] = a aux ≥ 0

The following line is added to the end of the formula:

t ≥ 0 ∧ state ok (a ok , a aux , t + 1) =⇒ a ok [t]
Example 10. Here is presented an example with generating the modulus of a number. If the number is positive then nothing happens, otherwise the negation of the number is returned. This In order to be able to iterate over the array, we should also store information about the size of the array and the current index. As the value of size is xed and known at compile time, there is no need to make a predicate parameter of it, we can simply insert the hard-coded value of size in the translation.

t ≥ 0 =⇒ state var1 (a x , a xpos , a var1 , a var2 , t + 1) ∧ a var1 [t] = a x [t] ≥ 0 t ≥ 0 =⇒ state var2 (a x , a xpos , a var1 , a var2 , t + 1) ∧ a var2 [t] = -a x [t] t ≥ 0 ∧ state var1 (a x ,

RT n°0492

The value of index, may change at each step, so it will be dened as a predicate parameter.

With this additional parameter in the state predicates, the arity of the states is dierent from the arity calculated using equation [START_REF]Verimag Research Center[END_REF]. The equation now becomes:

arity = N input_vars + N output_vars + N local_vars + N index_vars + 1, (3)
where N index_vars is equal to the number of dierent sized arrays.

Example 11. Variable observability In favor of uniformity, we consider that only one array element will be initialized per clause. With every operation, we start from index = 0, and iterate over the elements of the array, until index reaches the value of size. This means that all the elements of the array were initialized. A state predicate of an array variable has the additional condition of index = size in order to be valid.

Translation without abstraction

Map iterator Knowing that the size of the arrays part of the Map iterator must be equal, a single index and size parameter can be used. The Horn clause translation of a node containing a generalized map iterator with 2 inputs and 1 output, where the operation efectuated on the array elements is given by map_op and s is a hard-coded value:

t ≥ 0 ∧ state a (mda a , mda b , mda x , s, t + 1) ∧ state b (mda a , mda b , mda x , s, t + 1) =⇒ state x (mda a , mda b , mda x , 0, t + 1)

t ≥ 0 ∧ state x (mda a , mda b , mda x , index, t + 1) ∧ index < s =⇒ state x (mda a , mda b , mda x , index + 1, t + 1) ∧ mda x [index][t] = map_op(mda a [index][t], mda b [index][t])
Example 12. Let us consider the following Lustre V6 node, which maps the +(plus) operator on the elements of the 2 input arrays(a,b) and stores the result in the output array(x).

node usemap(a,b:int^2) returns (x:int^2); let x = map<<+,2>>(a,b); tel

The Horn clause encoding of the node contains a state predicate state x and a predicate in order to store the size of the array: t ≥ 0 =⇒ state x (mda a , mda b , mda x , 0, t + 1)

t ≥ 0 ∧ state x (mda a , mda b , mda x , index, t + 1) ∧ index < 2 =⇒ state x (mda a , mda b , mda x , index + 1, t + 1) ∧ mda x [index][t] = mda a [index][t] + mda b [index][t]
Red iterator The red (reduce) iterator reduces an array to a scalar variable. Note that in order to obtain the nal result we have to iterate over the array and save the partial results in an addition accumulator variable. This can be done without introducing a new element in the parameter list of the state predicate, if we store the partial results in the same variable where the nal result will be stored.

t ≥ 0 ∧ state init (a init , mda arr , a x , index, t + 1) ∧ state arr (a init , mda arr , a x , index, t + 1) =⇒ state x (a init , mda arr , a x , 0, t + 1)

t ≥ 0 ∧ state x (a init , mda arr , a x , index, t + 1) ∧ index = 0 =⇒ state x (a init , mda arr , a x , index + 1, t + 1) ∧ a x [t] = red_op(a init [t], mda arr [0][t]) t ≥ 0 ∧ state x (a init , mda arr , a x , index, t + 1) ∧ 0 < index ∧ index < s =⇒ state x (a init , mda arr , a x , index + 1, t + 1) ∧ a x [t] = red_op(a x [t], mda arr [index][t])
Example 13. We consider the following Lustre V6 node, with the red array iterator, having the input of an integer type array. The +(plus) operator is applied over the Red iterator. The sum of the array elements added to the value of initial input should be computed. If init = 0, then the result is the sum of the array elements. node usered(init:int;arr:int^4) returns (x:int); 2 let x = red<<+,4>>(init,arr); 4 tel

The translation of the above node: t ≥ 0 =⇒ state x (a init , mda arr , a x , 0, t + 1) t ≥ 0 ∧ state x (a init , mda arr , a x , index, t + 1) ∧ index = 0 =⇒ state x (a init , mda arr , a x , index

+ 1, t + 1) ∧ a x [t] = a init [t] + mda arr [index][t] t ≥ 0 ∧ state x (a init , mda arr , a x , index, t + 1) ∧ 0 < index ∧ index < 4 =⇒ state x (a init , mda arr , a x , index + 1, t + 1) ∧ a x [t] = a x [t] + mda arr [index][t]
When the value of index reaches 4, the current iteration has been terminated and the value of x is correctly set.

Fill iterator Respecting the constraints of our approach, which says that for each output and local variable we generate a state predicate, in the case of Fill iterator we have to generate multiple state predicate (for each individual output of the operation). The computation of a following element from the array needs that the partial result to be valid for the corresponding index. That means that, in a state predicate we not only have to store the value of the state predicate's variable, but we have to update all the variables, which take part in constructing the next element of the array.

The res, x = f ill << f ill_op, s >> (init) Lustre expression is translated as follows: state predicates for output x: t ≥ 0 ∧ state init (a init , mda x , a res , index, t + 1) =⇒ state x (a init , mda x , a res , 0, t + 1)

t ≥ 0 ∧ state x (a init , mda x , a res , index, t + 1) ∧ index = 0 =⇒ state x (a init , mda x , a res , index + 1, t + 1) ∧ (a res [t], mda x [index][t]) = f ill_op(a init [t]) RT n°0492 t ≥ 0 ∧ state x (a init , mda x , a res , index, t + 1) ∧ 0 < index ∧ index < s =⇒ state x (a init , mda x , a res , index + 1, t + 1) ∧ (a res [t], mda x [index][t]) = f ill_op(a res [t])
state predicates for output res: t ≥ 0 ∧ state init (a init , mda x , a res , index, t + 1) =⇒ state res (a init , mda x , a res , 0, t + 1)

t ≥ 0 ∧ state x (a init , mda x , a res , index, t + 1) ∧ index = 0 =⇒ state res (a init , mda x , a res , index + 1, t + 1) ∧ (a res [t], mda x [index][t]) = f ill_op(a init [t]) t ≥ 0 ∧ state x (a init , mda x , a res , index, t + 1) ∧ 0 < index ∧ index < s =⇒ state res (a init , mda x , a res , index + 1, t + 1) ∧ (a res [t], mda x [index][t]) = f ill_op(a res [t])
Example 14. The following program combines all the Lustre array iterators presented up until now. It has as input an array of integers and the maximum element from the array is selected.

In order to make sure that the maximum selection was done correctly, the following property is veried: all elements of the array are less of equal with the selected maximum.

The program is made of three Lustre nodes: a main observer node, where the property is computed and two auxiliary nodes used as operations in the array iterators. Note that in the below program has already been introduced the intermediate auxiliary variables to simplify the expressions:

--observer node --guarantees that max is greater than every element of the array node obs(in:int^4) returns (ok:bool) var max0,max,var1:int;

t ≥ 0 =⇒ state var2 (a c , a d , a x , a var2 , t + 1) ∧ a var2 [t] = a c [t] > a d [t] t ≥ 0 ∧ state var2 (a c , a d , a x , a var2 , t + 1) =⇒ state x (a c , a d , a x , a var2 , t + 1) ∧ a x [t] = ite(a var2 [t], a c [t], a d [t]) t ≥ 0 ∧ state x (a c , a d , a x , a var2 , t + 1) =⇒ interf ace selectM ax (a c , a d , a x , t + 1)
Node same is translated with:

t ≥ 0 =⇒ state m0 (a m , a m0 , a m1 , t + 1) ∧ a m0 [t] = a m [t] t ≥ 0 =⇒ state m1 (a m , a m0 , a m1 , t + 1) ∧ a m1 [t] = a m [t]
t ≥ 0 ∧ state m0 (a m , a m0 , a m1 , t + 1) ∧ state m1 (a m , a m0 , a m1 , t + 1) =⇒ interf ace same (a m , a m0 , a m1 , t + 1)

The observer node has the below translation. In order to keep the formulas simple we introduce the following notation: p ::= mda in , a ok , a var1 , a max , a max0 , mda ok_list , mda max_list

t ≥ 0 =⇒ state var1 (p, index, t + 1) ∧ a var1 [t] = mda in [0][t] t ≥ 0 ∧ state var1 (p, index, t + 1) =⇒ state max (p, 0, t + 1) t ≥ 0 ∧ state max (p, index, t + 1) ∧ interf ace selectM ax (a var1 , mda in [index], a x , t + 1) ∧ index = 0 =⇒ state max (p, index + 1, t + 1) ∧ a max [t] = a x [t] t ≥ 0 ∧ state max (p, index, t + 1) ∧ interf ace selectM ax (a max , mda in [index], a x , t + 1) ∧ 0 < index ∧ index < 4 =⇒ state max (p, index + 1, t + 1) ∧ a max [t] = a x [t]
The expression max0, max_list = f ill << same, 4 >> (max); is translated with 6 Horn clauses:

t ≥ 0 ∧ state max (p, 4, t + 1) =⇒ state max0 (p, 0, t + 1) t ≥ 0 ∧ state max0 (p, index, t + 1) ∧ interf ace same (a max , a m0 , a m1 , t + 1) ∧ index = 0 =⇒ state max0 (p, index + 1, t + 1) ∧ mda max_list [index][t] = a m1 [t] ∧ a max0 [t] = a m0 [t] t ≥ 0 ∧ state max0 (p, index, t + 1) ∧ interf ace same (a max0 , a m0 , a m1 , t + 1) ∧ 0 < index ∧ index < 4 =⇒ state max0 (p, index + 1, t + 1) ∧ mda max_list [index][t] = a m1 [t] ∧ a max0 [t] = a m0 [t] t ≥ 0 ∧ state max (p, 4, t + 1) =⇒ state max_list (p, 0, t + 1) t ≥ 0 ∧ state max_list (p, index, t + 1) ∧ interf ace same (a max , a m0 , a m1 , t + 1) ∧ index = 0 =⇒ state max_list (p, index + 1, t + 1) ∧ mda max_list [index][t] = a m1 [t] ∧ a max0 [t] = a m0 [t] t ≥ 0∧state max_list (p, index, t+1)∧interf ace same (a max0 , a m0 , a m1 , t+1)∧0 < index∧index < 4 =⇒ state max_list (p, index + 1, t + 1) ∧ mda max_list [index][t] = a m1 [t] ∧ a max0 [t] = a m0 [t]
Translation of ok_list = map <<≥, 4 >> (max_list, in):

t ≥ 0 ∧ state max_list (p, 4, t + 1) =⇒ state ok_list (p, 0, t + 1) t ≥ 0 ∧ state ok_list (p, index, t + 1) ∧ index < 4 =⇒ state ok_list (p, index+1, t+1)∧mda ok_list [index][t] = mda max_list [index][t] >= mda in [index][t] RT n°0492
The output of the observer node is computed with the last red iterator:

t ≥ 0 ∧ state ok_list (p, 4, t + 1) =⇒ state ok (p, 0, t + 1) t ≥ 0 ∧ state ok (p, index, t + 1) ∧ index = 0 =⇒ state ok (p, index + 1, t + 1) ∧ a ok [t] = (true ∧ mda ok_list [index][t]) t ≥ 0 ∧ state ok (p, index, t + 1) ∧ 0 < index ∧ index < 4 =⇒ state ok (p, index + 1, t + 1) ∧ a ok [t] = (a ok [t] ∧ mda ok_list [index][t])
In order to verify that the described property is satised or not the following line is added to the translation:

t ≥ 0 ∧ state ok (p, 4, t + 1) =⇒ a ok [t]
Fillred iterator Similarly to the Fill iterator, we have to dene states for each generated output by the iterator. The res, x = f illred << f illred_op, s >> (init, arr) expression is translated, as follows: state predicates for output x : t ≥ 0 ∧ state init (a init , mda arr , a res , mda x , index, t + 1) ∧ state arr (a init , mda arr , a res , mda x , s, t + 1) =⇒ state x (a init , mda arr , a res , mda x , 0, t + 1)

t ≥ 0 ∧ state x (a init , mda arr , a res , mda x , index, t + 1) ∧ index = 0 =⇒ state x (a init , mda arr , a res , mda x , index + 1, t + 1) ∧ (a res [t], mda x [0][t]) = f illred_op(a init [t], mda arr [0][t])
t ≥ 0 ∧ state x (a init , mda arr , a res , mda x , index, t + 1) ∧ 0 < index ∧ index < s =⇒ state x (a init , mda arr , a res , mda x , index

+ 1, t + 1) ∧ (a res [t], mda x [index][t]) = f illred_op(a res [t], mda arr [index][t])
state predicates for output res :

t ≥ 0 ∧ state init (a init , mda arr , a res , mda x , index, t + 1) ∧ state arr (a init , mda arr , a res , mda x , s, t + 1) =⇒ state res (a init , mda arr , a res , mda x , 0, t + 1) t ≥ 0 ∧ state x (a init , mda arr , a res , mda x , index, t + 1) ∧ index = 0 =⇒ state res (a init , mda arr , a res , mda x , index In order to be able to choose the state predicate, where the output is correctly initialized we make the following choice: when index reaches the value of size, we know that all elements has been processed and the accumulator is correctly set, so we can store the value of the output. To make dierence between this and the state where the output is also initialized, we set the value of the accumulator to -1, which state normally should be unreachable.

+ 1, t + 1) ∧ (a res [t], mda x [0][t]) = f illred_op(a init [t], mda arr [0][t]) t ≥ 0 ∧ state x (a init ,
In summary, in order to use the value of the boolred iterator's output we have to make sure that the state predicate of the output is valid with index = size and acc = -1.

Translation with abstaction

Red iterator with abstraction As we observed, formulas generated from programs using red iterators have an exponential behaviour with respect to the size of array. Using the Vaphor to get rid of arrays we could diminiuate the execution time and memory usage.

After having a basic translation, in of hope making an array size indepentent translations on programs containing array iterators, experiments were made to invent some form of abstractization, particularly on the Red iterator. In this case, we could generate formulas from programs using the red iterator without taking into account the size of the array. This would lead to constant execution time of the proving process.

The idea behind the abstraction is, that we can prove if a property is true, if the abstracted formula proves to be satisable. In other case, we can not conclude anything about the formula.

We generate two partial boolean results from dierent states of the iteration. The nal truth value of formula is given by the conjunction of the two partial results. They are computed in two steps, as follows (graphical illustration in Figure 5): 1. Verify the satisability of the property on the result computed by applying the operator on the init input variable and the rst element of the array, considering that the used operands meet the required preconditions. From here the value of ok1 is obtained.

2. We verify the property on a result computed in an arbitrary step,i, of the iteration by generating a result having as operands an accumulator, and the i th element of the array.

We assume that the previous results are correct, i.e., the accumulator satises the desired property. The same must be true also about the current array element. From here the value of ok2 is obtained. The nal result ok = ok1 + ok2.

Example 15. In this example the abstracted formula of a Red iterator is presented:

.. 2 r = red<<+;4>>(0,T); ok = r >= 0; 4 .. The ok property is the conjunction of two partial properties. In the below formula, elt1 and eltn are elements from the array T, which should satisfy the assumptions at the beginning of the program(if stated). They are stored in state r . To compute r2 = acc + eltn we assume that acc already satises the property:

t ≥ 0 ∧ state r (T, elt1, eltn, t + 1) ∧ state ok2 (acc, ok2, t + 1) ∧ ok2[t] =⇒ state r2 (r2, ok2, t + 1) ∧ r2[t] = acc[t] + eltn[t]
As initially, no state ok2 is valid, we have to make the rst step, and initialize the accumulator according to the property. Without this denition, because of the deadlock between the two above clauzes, the ok2 property will not be computed: The prototype produces a SMTLIB2 [START_REF] Barrett | The smt-lib standard: Version 2.0[END_REF] format le. After that the Vaphor [START_REF] Monniaux | Cell morphing: from array programs to array-free Horn clauses[END_REF] and Z3Prover [START_REF]Z3 Theorem Prover[END_REF] tools are used to argument about the satisability of the generated formula. Experiments were made on a machine with 4 i7-4510U 2.00Ghz cores, 8 GiB RAM.

t = 0 ∧ acc[t] ≥ 0 =⇒ state ok2 (, t + 1) ∧ ok2[t] = acc[t] ≥ 0 4

Results

Experimental results show that formulas generated from simple Lustre programs, without using arrays, can be almost instantly resolved by Z3. Note that, even if in the Lustre program we did not use arrays, after the translation all the variables become unidimensional arrays. However, for some programs, where complex safety properties are veried, the prover tends to give unknown or timeout (> 5 min) results.

Bounded intervals Experiments show that the prover can easily reason about if a variable is bounded in a specied interval or not, if we try to reason using the extremities of the interval.

However, for random variables, the execution of the prover times out.

Example 16. Prove sat vs. unsat During the experiments I have discovered, that sometimes it is easier to prove the unsatisability of a formula than it's satisability. So, in order to determine whether a formula F is satisable or not, we can reason about not F . If not F is an unsat formula, we conclude the correctness of F . In hope of reducing the complexity, the same program was fed to Vaphor [START_REF] Monniaux | Cell morphing: from array programs to array-free Horn clauses[END_REF] to abstract the arrays from the formula. We should notice a decrease in the prover's execution time, which is conrmed by the Figure 9. Note that using Vaphor, we were able to efectuate test to array sizes way above 16, the prover using signicantly less memory on the abstracted formulas than before.

A comparison between the execution time on the two formulas is given in Figure 10. In this report, we have proposed a method to verify safety properties on programs written in Lustre-V6 (including array iterators) by translating the original program into a formula of Horn clauses, which is then sent to a prover. A prototype translator was implemented inside the Lustre-V6 compiler generating Horn clauses from the internal representation of Lustre programs (Lustre Internal Code). We have used Vaphor to generate abstracted formulas (without arrays) and the stock version of Microsoft Research Z3Prover to reason on the formulas. While the prover was able to solve many of the generated formulas within seconds and formulas from programs with array iterators within minutes (for larges array sizes), some of the formulas still could not be solved in reasonable time (timeout error).

As experiments show, the simple syntactic translation done is this work does not produce great results applied on programs with larger sized arrays. The proving time becomes too long and memory usage too big. Using the Vaphor to make abstraction of arrays in the formula, we were able to successfully reason about programs with array iterators using larger sized arrays (>15), because the prover uses way less memory when solving formulas without arrays.

Pushing forward the experiments on array iterators, an abstraction of the Red iterator was formalized, eliminating entirely the use of multidimensional arrays in the generated formula.

Hand-written abstract translations of examples were tested. Including an automatic translation of the array iterators into abstracted (2-D array free) formulas would be a signicant improvement on the presented work.

  outputs and local variables (inside a node, local ows may be dened). Each output and local ow must be dened by exactly one equation, in any order. An equation may contain node calls, connecting nodes with each other. The Lustre program becomes a network of nodes, having a main node -the node of the program, which communicates with the outside world: accepts inputs and produces outputs.

Figure 1 :

 1 Figure 1: Lustre variables ow for the cpt node

Inria

  type ::= simple_type | array_type simple_type ::= bool | int | real array_type ::= simple_type ∧ size size ::= int Note that we are dealing only with unidimensional arrays. Multidimensional arrays are beyond the scope of this work. In section equations the following types of variable denitions are considered to exist: x ::= expr expr ::= numexpr | var 1 → var 2 | pre(var) | ite(bool_var, var, var) | iterator | nodecall numexp ::= var | op var | var op var iterator ::= map | red | ll | llred | boolred

Figure 2 :

 2 Figure 2: Array iterators in Lustre-V6

2 . 2

 22 Horn clausesThe target of our translation is to convert the initial Lustre program into Horn clauses, a widely used format for program verication. We aim to convert the program into Horn clauses by maintaining the majority of the types and operations from the source language.

Figure 3 :

 3 Figure 3: State automaton

Figure 4 :

 4 Figure 4: Variable value observability in Horn encoding of Lustre programs

Example 8 .

 8 Program to detect falling edges: node rising(x:bool) returns (y:bool); let y = false -> x and not pre(x); tel node falling(x:bool) returns (y:bool); let y = rising(not x); tel

  [t] Example 9. Consider the Lustre node from Example 7. If we wish to present an automatic translation of the node, rst of all we have to transform the Lustre program into and intermediate representation, splitting the non-trivial expressions and then apply the transformation rules on the new program. The previous program becomes: node inc() returns (x:int)

  way the output of the node modulus should always be positive. An observer node is attached to the program to verify this property. The Lustre program is: node modulus(x:int) returns(xpos:int); let xpos = if x >= 0 then x else -x; tel node obs(in:int) returns(ok:bool); var aux:int; let aux = modulus(in); ok = aux >= 0; tel The description of the same program in an intermediate language from which point an automatic translation is done: Inria node modulus(x:int) returns (xpos:int); var var1:bool; var2:int; let var1 = x >= 0; var2 = -(x); xpos = if var1 then x else var2; tel node obs(in:int) returns (ok:bool); var aux:int; let aux = modulus(in); ok = aux >= 0; tel Let us now dene the Horn encoding of the node modulus:

  ;4>>(var1, in); max0,max_list = fill<<same,4>>(max); ok_list = map<< >=, 4>>(max_list,in); ok = red<< and,4>>(true,ok_list); tel --returns the same input in two outputs node same(m:int) returns (m0,m1:int); let m0 = m; m1 = m; tel --returns the maximum of the two inputs node selectMax(c,d:int) returns (x:int) var var2:bool; let Inria 28 var2 = c > d; x = if var2 then c else d; 30 tel Now, let us dene each node in Horn encoding starting with the selectMax node:

Figure 5 :

 5 Figure 5: Abstraction of the red iterator

  Figure 6: Setup

Figure 7 :Figure 8 :

 78 Figure 7: Simple node with Map iteratorArray iterators The majority of the experiments were done over programs using array iterators. For dierent programs, the generated formula a linear/exponential increase, with respect to the size of the used arrays, is noticeable. For formula generated from a simple program presented in example 17 we notice a linear increase, as presented in Figure7.

Figure 10 :

 10 Figure 10: Comparison on execution time: Z3 vs. Vaphor+Z3After observing the exponential behaviour on a formula containing the red iterator, it is

  The format of the state predicate becomes: state x (a, n).

	For storing values into variables we use the following syntax: state init (a, n) ∧ a[0] = 42 ∧ n = 1
	meaning that we are in state init, where the rst element of the array is set to 42 and n is set to
	value 1.
	The previous systems' Horn clause description is, as follows:
	∀a, ∀n : state start (a, n) =⇒ state init (a, n)
	∀a, ∀n : state

  state end (a, n) true =⇒ state start (a, n).

	∀a, ∀n : With this clause added, we know from the beginning that state start (..) is true, i.e., the initial
	state of the system is dened. From now on implies statement is written, as precondition should
	have or true or ∀a, ∀n : state start (a, n) in order to be reachable.
	3 Contribution
	In this section the eective translation of a Lustre program into Horn clauses is described, giving
	step by step denitions for each used Lustre syntactic element. We start by formalizing the
	translation of variables, expressions, programs with multiple nodes, observer nodes, and array
	iterators.
	3.1	Translation of basic Lustre nodes into Horn clauses
	Variables We dene for each output and local variable a Horn state predicate. Currently, we
	do not dene state predicates for the input variables as they are considered to exist and the valid
	before the execution of the program. Having a Lustre node with 2 output variables(x,y), in Horn
	encoding 2 dierent state predicates will be generated: state x and state y . As parameters of a
	predicate, all the variables of the node will be included. The arity of a state predicate is given
	by
	Considering the above formula, the verication state end (a, n) ∧ a[19] = 19 should be true. There
	is only one element left to explain: how is the starting state, state start reached? The answer
	consists of adding the following clause to the formula:
	RT n°0492

  a xpos , a var1 , a var2 , t + 1) ∧ state var2 (a x , a xpos , a var1 , a var2 , t + 1) =⇒ state Translation of Lustre nodes with arrays into Horn clauses Representing arrays In this section we will dene a representation in Horn encoding of array types dened in Lustre. As we already dened an array for a variable to represent simple variables, for a Lustre unidimensional array, we have a multidimensional(2-D) array in Horn encoding, from now on noted with mda varname . So, if we want to access the element with index = 1 of the Lustre array a, at time-stamp t, we have to access the following element: mda

	3.2

xpos (a x , a xpos , a var1 , a var2 , t + 1) ∧ a xpos [t] = ite(a var1 [t], a x [t], a var2 [t])

t ≥ 0 ∧ state xpos (a x , a xpos , a var1 , a var2 , t + 1) =⇒ interf ace modulus (a x , a xpos , t + 1)

The translation of the observer node: t ≥ 0 ∧ interf ace modulus (a in , a aux , t + 1) =⇒ state aux (a in , a ok , a aux , t + 1)

t ≥ 0 ∧ state aux (a in , a ok , a aux , t + 1) =⇒ state ok (a in , a ok , a aux , t + 1) ∧ a ok [t] = a aux [t] ≥ 0

To make the property verication one last statement, which validates the output of the observer node, should be added: t ≥ 0 ∧ state ok (a in , a ok , a aux , t + 1) =⇒ a ok [t] a

[START_REF]Verimag Research Center[END_REF]

[t].

  Given the following header of a Lustre node, corresponding Horn clause state predicate is: state x (a start , a count , mda x , index x , t), where the parameter index x ∈ {0, 1, 2, 3}.

	node array_node(start:bool, count:int)
	returns(x:int^4);

the

  mda arr , a res , mda x , index, t + 1) ∧ 0 < index ∧ index < s =⇒ state res (a init , mda arr , a res , mda x , index+ 1, t + 1) ∧ (a res [t], mda x [index][t]) = f illred_op(a res [t], mda arr [index][t])Boolred iterator In case of the boolred iterator, we have to deal with additional parameters: min and max. Note that: min ≤ max ≤ size. As the values of the integers min and max must be known at compile time, we can use hard-coded values as we done with the array size. The Horn clause translation of the boolred iterator, having the state x (mda in , a x , acc, index, t) state predicate for an expression like x = boolred << min; max; s >> (in_bool) is:t ≥ 0 ∧ state in_bool (mda in_bool , a x , acc, s, t + 1) =⇒ state x (mda in_bool , a x , 0, 0, t + 1)Inria t ≥ 0 ∧ state x (mda in_bool , a x , acc, index, t + 1) ∧ index < s =⇒ state x (mda in_bool , a x , acc new , index + 1, t) ∧ acc new = ite(mda in_bool [index][t], acc + 1, acc) t ≥ 0 ∧ state x (mda in_bool , a x , acc, index, t + 1) ∧ index = s =⇒ state x (mda in_bool , a x , -1, index, t + 1) ∧ a x [t] = ite(min ≤ acc ∧ acc ≤ max, true, f alse)Note that, in this case the arity of the state predicate does not respect the equation 3, because 1 additional parameter was included to store the intermediate results of total number of true

	values.

  t ≥ 0 ∧ state ok (ok, t + 1) =⇒ ok[t] t ≥ 0 ∧ state ok1 (r1, ok1, t + 1) ∧ state ok2 (r2, ok2, t + 1) =⇒ state ok (ok, t + 1) ∧ (ok[t] = ok1[t] ∧ ok2[t])

Variables ok1 and ok2 are computed, if the corresponding results are valid:

t ≥ 0 ∧ state r1 (r1, t + 1) =⇒ state ok1 (r1, ok1, t + 1) ∧ ok1[t] = r1[t] ≥ 0 t ≥ 0 ∧ state r2 (r2, t + 1) =⇒ state ok2 (r2, ok2, t + 1) ∧ ok2[t] = r2[t] ≥ 0

We dene r1 = 0 + elt1: t ≥ 0 ∧ state r (T, elt1, eltn, t + 1) =⇒ state r1 (r1, ok1, t + 1) ∧ r1[t] = 0 + elt1

[t]

  For the below program, the result for dierent properties are presented:

	node obs(reset:bool) returns(ok:bool) ;
	var
	sevseg:int;
	let
	sevseg = 0 -> if (reset or pre(sevseg = 9))
	then 0 else pre(sevseg)+1;
	ok = sevseg < 10;
	tel
	ok = sevseg <= 9; gives sat
	ok = sevseg >= 9; gives unsat
	ok = sevseg <= 10; gives timeout
	ok = sevseg <= 0; gives unsat
	ok = sevseg <= 1; gives timeout
	ok = sevseg >= 1; gives unsat
	RT n°0492

Inria

RESEARCH CENTRE GRENOBLE -RHÔNE-ALPES