Autonomous systems such as unmanned vehicles and robots play an increasingly relevant role in our societies. Many factors contribute to the complexity in the design and development of those systems. First, they typically operate in dynamic and uncontrollable environments [1]–[5]. Therefore, they must continuously adapt their configuration in response to changes, both in their operating environment and in themselves. Since the frequency of change cannot be controlled, decision-making must be almost instantaneous to ensure timely responses. From a design and management perspective, it is desirable to minimize the effort needed to design the system and to enable its runtime updating and maintenance.

A promising technique to address those challenges is requirements-driven adaptation that endow systems with the necessary means to autonomously operate based on their requirements. Requirements are prescriptive statements of intent to be satisfied by cooperation of the agents forming the system [6]. They say what the system will do and not how it will do it [7]. Hence, software engineers are relieved from the onerous task of prescribing explicitly how to adapt the system when changes occur. Many current requirements-driven adaptation techniques [8], [9] follow the Monitor-Analyze-Plan-Execute-Knowledge (MAPE-K) paradigm [10], which usually works as follows [11]: the Monitor monitors the managed system and its environment, and updates the content of the Knowledge element accordingly; the Analyse activity uses the up-to-date knowledge to determine whether there is a need for adaptation of the managed element according to the adaptation goals that are available in the knowledge element. If adaptation is required, the Plan activity puts together a plan that consists of one or more adaptation actions. The adaptation plan is then executed by the Execute phase.

This approach has two main limitations in highly-dynamic operational environments. First, it tends to be myopic since the system adapts in response to changes without anticipating what the subsequent adaptation needs will be [5] and, thus, it does not guarantee the optimality of the overall behavior of the autonomous system. This is particularly crucial for systems that have to operate continuously without interruption over long periods of time, e.g., cyber-physical systems. Second, the time to plan adaptations could make timely reaction to changes impossible, particularly in fast changing environments. Therefore, an approach that enables an almost instantaneous reactions to changes is needed.

In this paper, we propose the Optimal by Design (OBD ) framework as a first step towards dealing with the aforementioned challenges. OBD supports a model-based approach to simplify the high-level design and description of autonomous systems, their capabilities, requirements and environment. Based on these high-level models, OBD constructs a Markov Decision Process (MDP) that can then be solved (possibly using state-of-the-art probabilistic model checkers) to produce optimal strategies for the autonomous system. These strategies define optimal reflex controllers that ensure the ability of autonomous systems to behave optimally and almost instantaneously to changes in itself or its environment.

Several previous works [5], [12]–[14] encode adaptation problems using general-purpose languages such as those proposed by probabilistic model checkers, e.g., PRISM [15]. Unfortunately, these languages do not offer primitives tailored to the design and analysis of autonomous systems. This makes them unsuitable to adequately describe the software requirements [6] of the autonomous system and the environment in which it operates. Examples of limitations of these languages resolved in this paper through OBD are the Markovian assumption [16] and the implicit-event model [17].

In a nutshell, OBD introduces a novel Domain Specific Modeling Language (DSL) for the description of autonomous systems, its environment and requirements. The semantics of the DSL is then defined in terms of a translation into a Markov Decision Process (MDP) model to enable the synthesis of optimal controllers for the autonomous system. This separation between the model (i.e. the DSL) and its underlying computational paradigm (i.e. MDP), brings several important advantages. First, the level of abstraction at which systems have to be designed is raised, simplifying their modeling by software engineers. Second, requirements become first-class entities, making it possible to elicit them using traditional requirements engineering techniques [6], [18]–[20] and to benefit from goal refinement, analysis and verification techniques developed for goal modeling languages. Moreover, this approach clarifies the limitations of the underlying computational model, namely the aforementioned Markovian assumption and the implicit-event model, and permits the identification and implementation of extensions necessary to overcome those limitations and support the required analysis, verification and reasoning tasks.

The remainder of this paper is structured as follows. Section II presents a motivating example, which will be used as a running example throughout the paper. Section III presents an overview of the OBD framework. Section IV introduces the framework’s model and language. Section V provides the semantics of OBD models by presenting their translation into MDPs. Section VIpresents an evaluation of the framework. Section VII discusses limitations and threats to validity. Finally, Section VIII discusses related work and Section IX concludes the paper and presents future work.

Our running example, inspired by one of the examples in [21], is the restaurant FoodX. Serving at FoodX is RoboX, an autonomous mobile robot. The restaurant comprises three separate sections: (1) the kitchen, (2) the dining area and (3) the office. RoboX is equipped with various sensors to monitor its environment and actuators to move around the restaurant and perform different tasks.

Several challenges must be dealt with in order to develop a controller for RoboX. First, there are events that occur in the environment beyond RoboX’s control. For example, a client may request to order or a weak battery signal may be detected. There is also the uncertainty in action effects caused by imperfect actuators, e.g. moving to the kitchen from the dining room could sometimes fail, possibly due to the movement of customers in the restaurant. RoboX may also have multiple (possibly conflicting) requirements: it may have to serve customers’ food while it is still hot but also has to keep its batteries charged at all times. Thus, RoboX should be able to prioritize the satisfaction of its requirements, taking into account the effects of their satisfaction over the long-term. It is also desirable that RoboX acts proactively. For instance, waiting in the dining area should be preferred to staying in, for example, the kitchen if doing so would increase the likelihood of it getting orders from customers.

Since the time and frequency of change in the environment cannot be controlled, enabling immediate and optimal responses to changes is highly desirable. In reactive approaches, classical planning (e.g., STRIPS [22] and PDDL [23] planners) is often used to determine the best course of action after detection of change. This approach has important limitations. For example, imagine a situation where, while RoboX is moving to serve a customer in the dining room, a weak battery signal is detected. In this case, RoboX can either halt the execution of the current plan until a new plan is computed or continue pursuing serving the customer, having no guarantees that this plan is still the optimal course of action. If the frequency of changes in the environment is high, then the autonomous system may get permanently stuck computing new plans, or be always following sub-optimal plans.

This example highlights the five requirements for the software to control RoboX which we explore in this paper:

1) Handling of uncertainty in event occurrences and effects;

2) Proactive and long-term behavior optimization to consider the possible evolution of the system when determining the best course of action;

3) Fast and optimal response to changes to ensure their ability to operate in highly dynamic environments;

4) Support of requirements trade-offs and prioritisation; 5) Support of requirements-driven adaptation to raise the level of abstraction of system design.

OBD is a framework for the model-based requirements-driven synthesis of optimal adaptation strategies for autonomous systems. The model-based approach raises the level of abstraction at which systems need to be described and simplifies model maintenance and update. Adaptation in OBD is requirements-driven, enabling systems to autonomously determine the best way to pursue their objectives. Based on OBD models, Markov Decision Processes (MDPs) are constructed. Solving those MDPs determines the system’s optimal strategy, i.e., the behavior that maximizes the satisfaction of requirements. In a strategy, the best adaptation action that should be taken in every possible (anticipated) future evolution of the system is identified, eliminating the need to re-analyze and re-plan after every change and enabling almost instantaneous reactions. Indeed, an optimal strategy defines a reflex controller that can react optimally and in a timely way.

Figure 1 depicts an overview of the framework, which includes a model (and a language) to describe the basic elements of self-adaptive systems [11]: the environment refers to the part of the external world with which the system interacts and in which the effects of the system will be observed and evaluated; the requirements or adaptation goals are the concerns that need

Fig. 1. Framework Overview

to be satisfied; the managed system represents the application code or capabilities/actuators that can be leveraged to satisfy the requirements. Based on these elements, the controller or the managing system ensures that the adaptation goals are satisfied in the managed system, is synthesized.

The computation of optimal strategies is based on a domain model. A domain model specifies the environment, the capabilities of the autonomous system (or agent) and its requirements. Formally, an OBD model () is a tuple where:

• SV is a finite set of state variables with finite domains. State variables describe the possible states, i.e., the con-figuration of the software system and the environment;

• AD is a finite set of action descriptions representing the means that are available to the agent to change the system state, i.e. update the state variables SV;

• ED is a finite set of event descriptions to represent the uncontrollable occurrences in the environment, i.e., events that change the state beyond the agent’s control.

• RQ is a finite set of requirements, i.e., the (operationalisable) goals that the software system should satisfy;

• is the initial state of the system determined by the agent’s monitoring components and sensors. An OBD model has a corresponding textual representation called its domain description. It is formalized in the following using a variant of Backus-Naur Form (BNF): the names enclosed in angular brackets identify non-terminals, names in bold or enclosed within quotation marks are terminals, optional items are enclosed in square brackets, | is ”or”, items repeated one or more times are suffixed with + and parentheses are used to group items together.

A. State, Actions and Events

State Variables (SV): define the possible states, i.e., configurations of the software system and the environment. A variable is a multi-valued variable with a corresponding domain, denoted dom(x). Every value is a configuration of x. A state variable is defined as follows:

where is text, i.e., a concatenation of letters, digits and symbols. For example, we can represent the location of RoboX and the status of tables at the restaurant using the following variables:

The variable location defines the possible locations of RoboX. The variables represent the status of tables: when there are no customers at , then . When a customer arrives and sits at the table, becomes occupied. Figure 2 depicts the update of the value of with the occurrence of the robot actions {get order, give order, collect order, deliver order, clean table} and the exogenous events {customer arrives, customer orders, kitchen notification, customer pays}. In contrast to actions, exogenous events have an occurrence probability denoting their likelihood in a given situation. Actions, on the other hand, have a cost that represent the effort or price of their execution. Both exogenous events and actions do not have to be deterministic, i.e., their execution can have various effects, each with a different probability (in pink in the figure).

Variables which are not explicitly defined are considered to be boolean, i.e., their domain is {tt, ff}. The notations id and !id are used as shortcuts for id=tt and id=ff, respectively. The following declaration defines a boolean variable to represent that customers sitting at a table had looked at the menu.

Actions (AD): are means that are available to the agent to change the system state. An action description is an expression that is defined as follows:

Actions can have a cost representing the difficulty level or effort necessary to execute it. Action costs are useful to tradeoff the satisfaction of requirements with the required effort and, when not specified, are set to zero. In the following example, the cost of moving to is set to 10.

Note that an expression is well-formed only if (1) its various are disjoint, i.e., they cannot be satisfied

<get_order> : 10[Exogeneous Event] : Occurrence Probability

Fig. 2. A simplified model of serving a table at restaurant FoodX.

at the same time and (2) for every , the sum of the probabilities of its subexpressions is one, i.e., . Note that we allow to be less than one. In this case, action execution has no effect with a probability of . For example, this makes it possible to remove the second effect, prob , from the previous action description without affecting the action semantics.

Events (EV): represent occurrences that are not controlled by the agent. They may happen in the environment at any moment. An event description is expressed as follows:

Events are conditional and can occur with a different probability depending on the situation. For instance, we can represent that customers may order with a higher probability if they had looked at the menu as follows:

B. Requirements

Requirements represent the objectives of the autonomous system. Every requirement is associated with a reward denoting its importance. OBD currently supports fourteen requirement types, which build upon and extend the goal patterns of the KAOS goal taxonomy [24]. Requirements are expressions:

⟨

⟨

A requirement’s type is determined based on whether it: is conditional (C) or unconditional (U); is a maintain (M) or achieve (A) requirement: duration of maintain requirements can be time-limited and its compliance can be best-effort (P) or strict (PR), i.e., during its duration the requirement does not have to be “always” satisfied; has a deadline (D), which can be exact (E), i.e., the requirement has to be satisfied at the deadline, or flexible (F), the requirement has to be satisfied

within the deadline. Due to space limitations, we only present unconditional, conditional and achieve deadline requirements.

Unconditional Requirements: denote conditions that have to be always maintained or (repeatedly) achieved.

For example, a requirement to remain in the dining room or an to ensure that repeatedly pays.

Conditional Requirements: should be satisfied only after some given conditions are true. They can have a cancellation condition after which their satisfaction is no longer required.

For example, RoboX may have to get the order from only if requests to order, or it should remain in the dining room after it gets until ’s order is served.

Deadline Requirements: must be satisfied after an exact number of time instants or within a period of time:

For example, RoboX may have to be at within at most 4 time units after requests to place an order, or it may have to be at the kitchen after exactly 4 time units after it receives a notification that food is ready.

In the following, we use the terms name, required condition, activation condition, cancellation condition and deadline to refer to the parts of a requirement expression that come after ReqID’, achieve’ or maintain’, if’, unless’ and after’ or within’ parts of the requirement expression respectively.

Markov Decision Processes (MDPs) are mathematical frameworks for modeling and controlling stochastic dynamical systems [17]. Informally, MDPs may be viewed as Labeled Transition Systems (LTSs) where transitions are probabilistic and can be associated to rewards. Intuitively, solving an MDP means finding an optimal strategy, i.e., determining the actions to execute in every state in order to maximize the total expected rewards. In the following, we first introduce MDPs (Section V-A), then we discuss the main steps needed to construct an MDP starting from an OBD domain model (Section V-B).

A. Introduction to MDPs with Rewards

A reward MDP is a tuple , where:

• S is the finite set of all possible states of the system, also called the state space;

• A is a finite set of actions; • where D(S) is the set of probability distributions over states S. A distribution is a function such that . The transition relation specifies the probabilities of going from state after execution of action a to states . In the following, we will use the (matrix) notation to represent the probability of going to after execution of a in ; • is a reward function specifying a finite numeric reward value when the system goes from state to state as a result of executing action a. Thus, rewards may be viewed as incentives for executing actions. We will use to represent . Formally, a (memoryless) strategy is a mapping from states to actions. An optimal strategy, denoted , is the one which maximizes the expected linear additive utility, formally defined as . Intuitively, this utility states that a strategy is as good as the amount of discounted reward it is expected to yield [25]. Setting expresses indifference of the agent to the time in which a particular reward arrives; setting it to a value reflects various degrees of preference to rewards earned sooner. MDPs have a key property: solving an MDP finds an optimal strategy , which is deterministic, Markovian and stationary. This means that computed strategies are independent of both past actions/states and time, which ensures their compactness and practicality. Furthermore, there exist practical algorithms for solving MDPs, e.g., value iteration and policy iteration. Both of these algorithms can be shown to perform in polynomial time for fixed [26]. MDPs with memoryless strategies, depicted in Figure 3 (rounds are states and rounded squares are events), have however the following restrictions: The implicit-event action model [17]: MDPs do not support an explicit representation of exogenous events. Figure 4 shows exogenous events (in non-rounded squares connected

with pointed line to states) that can occur with certain occurrence probabilities (in green in the figure) in every state. Exogenous events are an essential element to model aspects of the environment that are not controllable by the agent. They are the means to represent, for example, that customers can arrive at the restaurant or that they may request to order.

The Markovian assumption [16], [27]: in MDP, reward and transition functions have to be Markovian, i.e., they can not refer to the history of previous states or transitions. Figure 5 shows an example of a non-Markovian reward (described on the dashed transition), i.e., one that is entailed only if certain conditions are satisfied on the history of states and transitions. The support of non-Markovian rewards is necessary to associate transitions that satisfy requirements [6], which are often conditional and can have deadlines, with rewards.

B. Overview of the Construction of MDPs from OBD Models

The construction of MDPs based on OBD models1 relies on the following intuitions:

• the states and the (probabilistic) transitions of the LTS behind the MDP are constructed based on the variables, actions and events in the OBD domain model;

• the rewards in the MDP are associated with transitions that lead to the satisfaction of requirements. Dealing with the Markovian assumption: Building an MDP from an OBD model requires the satisfaction of the Markovian assumption. In the context of this work, determining the satisfaction of requirements, with the exception of unconditional requirements, requires to keep track of history. To solve this issue, we extend the state space to store information that is relevant to determine the status of requirements in every state. This is done by associating every requirement with a state variable, whose value reflects the status of the requirement in the state2. The value of those variables, called requirements variables, are updated whenever their corresponding requirement is activated, canceled, satisfied, etc. Requirements Variables RV are special variables whose domain represents all the possible statuses of their corresponding requirement. The statuses of requirements and their update after requirement activation, cancellation, satisfaction, etc are defined in the transitions part of Figures 8 and 9. On the other hand, the rewards part defines transitions that satisfy requirements and, consequently, entail a reward. For example, consider a conditional achieve requirement CA of the form ReqID m achieve S if A unless Z reward r. This requirement is associated with a requirement variable m whose domain includes the requirement’s possible statutes {I, R}. The transitions part of Figure 9 shows the evolution of CA requirements when their activation, cancellation and required conditions occur. It is to be read as follows: when the status is I and the activation condition A is true, then the

Fig. 3. Basic MDP model

Fig. 4. Support of Exogenous Events

Fig. 5. Support of Non-Markovian Rewards

status is updated to R. Analogously, if the status is R and the cancellation condition Z or the required condition S is true, then the status is updated to I. The updating of a state variable as just described enables the definition of a Markovian reward when requirements are satisfied. The rewards part of Figure 9 shows transitions of CA requirements that entail rewards. This figure should be read as follows: a requirement m of type CA induces a reward r on a transition from a state i to a state j iff, in i, the required condition of m does not hold and the status of m is R; while S holds in j.

Dealing with the absence of exogenous events: OBD models have explicit-event models whereas MDPs impose an implicit-event action model. To overcome this limitation, we exploit the technique proposed in [17] which enables computation of implicit-event action transition matrices from explicit-event models. The use of this technique assumes the following rules: 1) the action in which exogenous events are folded, always occurs before it and 2) events are commutative, i.e., their order of occurrence from an initial state produces the same final state. Under those assumptions, which are satisfied in our running example, the implicit-event transition matrix of an action a is computed in two steps: first, the transition matrix of a (without exogenous events) and the transition matrix and occurrence vector of every event e are computed separately; then, those elements are used to construct the implicit-event matrix of every action a. This process is illustrated in the following section using an example. Note that it is possible to integrate other (more complex) interleaving semantics into the framework if necessary by changing the technique used to compute the implicit-event transition matrix [17].

C. MDP Construction Process

An OBD MDP is constructed from a model as follows.

States S: represent all possible configurations of the system and the environment. A state is a specific configuration, i.e., an assignment of every state variable in SV and requirement variable in RV a value from their domain.

For example, consider a domain model comprising of two boolean variables x and y and one requirement m of type CA. The set of states S constructed from comprises all possible configurations of its state and requirement variables. Thus, S includes the eight states in Figure 6.

Fig. 6. Constructed States

Fig. 7. (1) action transitions, (2) implicit-event action transitions.

Actions A: are all the actions appearing in AV of the domain model extended with the empty action noop, which produces no effects and has no cost, i.e., .

The transition matrix T : is computed in two steps: first, the transition matrix of a (without exogenous events) and the transition matrix and occurrence vector of every event e are computed separately; then, those elements are used to construct the implicit-event matrix of every action a.

For example, consider that our domain model includes one probabilistic action a, one deterministic action b and one requirement m, which are defined as follows:

Figure 7(1) shows the transitions caused by the execution of actions in the states and . For example, since the condition !x is satisfied in , the execution of a in produces x with a probability of 0.8 and produces y with a probability of 0.2. Notice that after the execution of a, the base state of both and could be the result of executing action a in . However, since the execution of a satisfies the requirement m, i.e., makes x true, only the expanded state of satisfies the state transition model of the CA requirement m shown in Figure 9 since m = I. Thus, the execution of a in state leads to with a probability 0.8, i.e., . The execution of b and noop do not change the state.

Events are similar to actions with the exception that they have occurrence probabilities, do not have a cost and do not

Fig. 8. Unconditional Requirements States and Rewards

advance time since they occur concurrently with actions. Let e be an event defined similarly to a as follows:

In this case, the transition matrix of e is similar to that of a, i.e., . The occurrence vector of e represents the probability of occurrence of e in every state. Since the condition is satisfied in the states and , . Figure 7(2) shows the implicit-event transitions for the states and : in , event e may occur with a probability of 0.2, thus its effects are factored in action transitions as shown in Figure 7(2); in , the condition of e is not satisfied and, therefore, it does not affect the computed transitions for the actions noop and a. Due to the interleaving semantics where exogenous events (may) occur after action execution, the transition caused by b in is affected due to the possibility that e occurs after b.

Construction of the reward matrix R:: Transition rewards are affected by: (1) action costs and (2) satisfaction of requirements. In particular, a transition reward is the sum of rewards obtained due to satisfaction of requirements on the transition from to minus the cost of a. For example, consider the transition from to caused by the execution of a in . On this transition, the requirement m is satisfied. Since the cost of executing a is 10, this transition will be associated with a reward of , i.e., .

D. Requirements Transitions and Rewards

This section explains the key intuitions behind the modeling of requirements in OBD and their semantics. Unconditional Achieve and Maintain Rewards: A maintain requirement defines a condition that should be kept satisfied. Therefore, a reward is given to the agent whenever this condition holds over two consecutive states, see, e.g., in Figure 8. On the other hand, an achieve requirement defines a condition that should be reached. Therefore, the agent is rewarded when this condition becomes true, i.e., when it does not hold in a state but holds in the next, e.g., see . Conditional Requirements: The satisfaction of requirements is often necessary only after some condition A becomes true, see for instance and in Figure 9. Those requirements are therefore modeled as state machines which are initially in an initial or inactive state I. When their activation condition A occurs, a transition to a new state R occurs. In a state R, the requirement is said to be in force, i.e., its satisfaction is required. While in R, the reward r is obtained whenever the agent manages to comply with the required condition S. If the cancellation conditions Z is detected while

the requirement is in force, a transition to I occurs, i.e., the requirement is canceled and has no longer to be fulfilled.

Deadline Achieve Requirements: Requirements are sometimes associated with fixed deadlines. Fixed deadlines can represent either an exact time after which the agent should comply with the requirement, see for example in Figure 9; or a period of (discrete) time during which the agent may comply at any moment, see for example . In both cases, deadlines are modeled similarly. For example, consider a requirement m having a deadline D. After m’s activation, a transition to a state A(D) occurs. At every subsequent time unit, a transition from a state A(X) to a state occurs (unless X = 1). A transition entails the requirement’s reward if the requirement is satisfied on this transition.

In this section, we first present an empirical evaluation of the framework by comparing the use of an OBD controller to control RoboX in a simulated software environment of the restaurant FoodX to a generic Monitor Analyze Plan Execute (MAPE) controller (Section VI-A). The MAPE controller relies on a Planning Domain Description Language (PDDL) planner, similarly to state-of-the-art robotic systems such as ROS [28]. Then, we present a qualitative comparison of OBD with state-of-the-art probabilistic model-checkers, PAT [29], PRISM [15] and STORM [30] which have been used in several other previous works [5], [12]–[14] to solve adaptation problems (Section VI-B). Finally, we describe the current prototype tool implementation and conduct a performance evaluation (Section VI-C).

A. Empirical Evaluation

Figure 10 depicts our simulation environment. It consists of a system state, an agent and an environment. The simulation runs in discrete time steps. At each step, the agent has to choose, based on the current system state, one action to execute from actions whose preconditions are satisfied in the state. On the other hand, some events are selected for execution, according to their occurrence probability, if their preconditions are true. After each time step, the state is updated by applying the effects of the chosen action and events in the current state. Effects of both actions and events are applied probabilistically according to the probabilities specified in their action/event descriptions, i.e. their execution can lead to different states. Experiments are run for one hundred thousands steps. To select the agent’s actions, two controllers were implemented: an OBD controller and a generic MAPE controller. The design rational of the experiment aims at comparing a OBD controller and generic MAPE controllers with respect to: types of supported requirements, enforcement model, response time, quality of decision-making and problem representation. Experiment Description: The experiment ran on a MacBook pro with a 2.2GHz Intel Core i7 and 16 GB of DDR3 RAM. At each time step, the agent queries the state (the (M)onitoring activity). The agent determines its action to execute by interacting with its controller. The controller, given

Fig. 9. Conditional and Achieve Deadline Requirements States and Rewards

the current state, determines the next action of the agent. The OBD controller is implemented in Java and uses the computed OBD strategies to determine the optimal action that the agent should take at each state. The MAPE controller is also implemented in Java. It consists of three components: 1) an analysis component that determines whether planning is needed, 2) PDDL4J, an open source Java library for Automated Planning based on PDDL [31], to compute plans and 3) a plan enforcer which returns one action at each step to the agent. Below is a comparison of the two controllers.

Supported requirements: OBD supports the types of requirements presented in Section IV-B. The MAPE controller, since it relies on a PDDL planer, can naturally encode unconditional and conditional achieve requirements, i.e. . The other types of requirements cannot be easily encoded in the form of PDDL planning problems.

Enforcement model: The OBD controller enforces MDP strategies. It has a simple enforcement model: it consults the computed strategy and determines the optimal action that corresponds to the current state at each time step. The MAPE controller enforces requirements as follows: if the activation condition of a conditional requirement is true in the state then a planning problem (Pb) is formulated to satisfy the requirement’s condition. When multiple requirements must be satisfied, then the goal state of the planning problem corresponds to the disjunction of their (satisfaction) conditions, i.e. one requirement should be satisfied. If a plan (P) is found by the PDDL planner, the plan enforcer module selects one action of P to return to the agent at each time step. A plan is pursued until its end, i.e. no re-planning is performed until the plan’s last action is executed unless a plan execution fails. A plan fails if one of its actions cannot be executed because its preconditions are not satisfied in the current state. This situation may occur due to nondeterministic action effects or event occurrences3.

Response time: Figure 11 shows the average time of decision making, i.e. the total decision-making time divided by the total number of steps of the experiment. Several domain descriptions differing in their total number of planning goals/requirements and action success rate4 (100%-50%) are considered. The decision time of an OBD controller is constant and almost instantaneous (200ns) as it consists of a simple lookup in the policy (which is stored in the form of an array of Integers) of the optimal action that corresponds to the current state. On the other hand, the analysis and planning activities of the MAPE controller introduce a significant overhead when compared to the OBD controller. The average decision-making time of MAPE controllers also increases with action nondeterminism as re-planning is required more frequently due to more frequent plan failures.

Quality of decision-making: Figure 12 shows the number of satisfied goals per time step for MAPE and OBD controllers. It demonstrates that the OBD controllers consistently outperform MAPE controllers for the same domain problems. This is due, on one hand, to their ability to include probabilities of event occurrences into their computation of optimal strategies. For instance, imagine that RoboX has to pass the order of a table to the kitchen but that it estimates that there is a highlikelihood that another table orders. In this case, the OBD controller may delay moving to the kitchen to pass the order and wait until the other table orders first before passing the two orders to the kitchen together. MAPE controllers are incapable of incorporating such intelligence in their decision-making. Another reason explaining this result is that MAPE controllers, once a plan is computed, commit to it unless the plan fails to avoid getting stuck in re-planning without acting, which could happen if the frequency of change in the environment is high. This makes it impossible to guarantee the optimality of plans throughout their execution. On the other hand, OBD strategies are guaranteed to always select the optimal action at each state.

Representation: An important difference is the goal/requirement representation. In MAPE, planning goals have to be satisfiable using solely the actions that are available to the agent. For example, consider a goal to achieve that a table pays as many times as possible. The satisfaction of this goal requires interactions with the environment as described in Figure 2. This requirement cannot therefore be expressed as a single planning goal but has to be decomposed into a set of planning goals, each of which has to be satisfiable by the actions available to the agent. On the other hand, thanks to the folding of events into actions, such requirements can be expressed directly in OBD. Consequently, expression of requirements in OBD can be much more succinct and enable system designers to focus of what should be satisfied rather than how they should be satisfied. In the running example, it

Fig. 10. Experiment Description

Fig. 11. Decision-making time per time step

Fig. 12. Goal satisfaction per time step

was possible to represent four MAPE planning goals in the form of a single OBD requirement.

B. Qualitative Comparison of OBD with State-of-the-Art Probabilistic Model-checkers

State-of-the-art probabilistic model-checkers PAT [29], PRISM [15] and STORM [30] support the description of various models using a variety of languages. In this work, we focus on MDP models because they support, as opposed to other models such as for example Discrete-Time Markov Chains, the synthesis of optimal strategies. With respect to the general-purpose languages proposed by probabilistic model-checkers, our model and language support exogenous events and various typical software requirements (Section IV-B), elements that cannot be modeled or expressed using the general-purpose MDP languages of PAT, PRISM or Storm. An extension of PRISM, namely PRISM-games, supports modeling of turn-based multi-player stochastic games. This enables the modeling of the environment as a separate player whose actions represent exogenous events. With respect to modeling of autonomous systems and their requirements, PRISM-games has two main limitations. First, similarly to PRISM, rewards have to be Markovain which means that there is no way to encode typical software requirements [6] such as those presented in Section IV-B using the provided (Markovian) reward structures. Furthermore, modeling of interactions between the agent and its environment in OBD where multiple events occur with each action of the decision maker is more realistic and natural than, in turn-based PRISM-games, where the environment may only be represented in the form of a separate player who selects at most one event to execute after each action of the decision maker.

C. Preliminary Experimental Evaluation

We have implemented the OBD framework as a Javabased prototype which uses EMFText [32], the MDPToolBox package [33] and Graphviz [34]. There are at least two main use cases of the framework: At design-time: the textual editor generated by EMFText can be used to define OBD models. The corresponding MDP models and optimal strategies can be then visualized and

Fig. 13. MDP Construction

Fig. 14. MDP Solution

inspected by a system designer and/or used to synthesize optimal controllers for the target autonomous systems; At runtime: the OBD Java API can be used to create instances of the OBD model and the computation of optimal strategies at runtime. At runtime, strategies should be recomputed after change in either 1) requirements or 2) domain descriptions. The former generally denotes a change in system objectives or their priorities. On the other hand, the latter is needed if new information (possibly based on interactions with the environment) shows that model parameters need to be revised. There are some limitations to this use scenario which are discussed in Section VII. Figures 13 and 14 show the MDP construction and solving time for different state space sizes, respectively. It is clear from the figures that the current implementation suffers from the state explosion problem. However, the support of thousands of states is typically sufficient for a large number of problems. Furthermore, solving an MDP is a one-time effort, i.e. once an MDP is solved (given a set of requirements), the computed strategies can be used until either requirements or the domain model change.The improvement of the performance of our current prototype represents future work.

This section discusses the current limitations and issues related to using OBD and means to address them. Setting of Model parameters: determining probabilities of actions and events can be challenging. We envisage that they shall be computed by adapting existing techniques that enable computation and learning of model parameters at runtime. For example, we could use [35] where Bayesian techniques are used to re-estimate probabilities in formal models such as Markov chains based on real data observed at runtime;

TABLE I COMPARISON OF OBD WITH RELATED FRAMEWORKS

or [36] which proposes an on-line learning method that infers and dynamically adjusts probabilities of Markov models from observations of system behaviour. Alternatively, reinforcement learning techniques [37] could be used.

Identification of requirements: strategies are computed according to requirements. It is thus crucial that they be correctly identified. OBD supports traditional goal modeling techniques [38]–[40]. Those techniques have been proven reliable over the years in ensuring correct elicitation, refinement, analysis and verification of requirements [38]–[40].

Suitability of the Application Domain: it is necessary to identify system conditions under which the framework may be used. Towards answering this question, we first define a predictable (unpredictable) system as one where probabilities of occurrence and effects of events/actions do not (do) change with time. Similarly, we define a dynamic (erratic) system as one where the rate of relevant5 change in those probabilities is within the order of hours or days (minutes or seconds). Our current prototype implementation computes strategies within minutes. Consequently, we conjecture that it supports the run-time synthesis of controllers in predicable and unpredictable dynamic systems. Erratic systems are not supported. A more precise definition of those limitations represents future work.

Table I compares the features of OBD with some notable requirements-driven adaptation frameworks according to the criteria in Sec. II, divided along the following dimensions.

Modeling compares the frameworks with respect to their support of the explicit modeling and representation of requirements, capabilities and events. Those feature are desirable as they simplify system design, its maintenance and modularity.

Uncertainty compares the support of uncertainty in exogenous event occurrences and effects.

Adaptation compares the type of adaptation strategies, which can be explicitly defined, configuration selection or behavior optimization. Configuration selection is a reactive approach where, after requirements are violated, the alternative system configurations are compared and the best one is selected. Behavior optimization is a proactive approach which takes into account not only the current conditions, but how they are estimated to evolve [12]. Only behavior-based optimization supports the two requirements of (1) proactive and long-term behavior optimization, and (2) fast and optimal response to change. Note that adaptation based on explicitly defined strategies is fast but provides no optimality guarantees.

Table I shows that adaptations in many current frameworks are either explicitly defined [6], [24], [41]–[44], [46] or determined based on a comparison of possible system configura-tions [8], [45], without taking into account future evolutions of the system. It also shows that explicit-event and action models are rarely considered. For example, QosMOS and KAMI consider Markov chains. This is why these frameworks have an implicit models of actions and events in Table I. Similarly, ActivForms rely on Timed Automata and the Execute activity is explicitly defined. Therefore, ActiveForms has explicit adaptation strategies and uncertainty is not handled. In [5], MDP is used to identify optimal adaptations at runtime, taking into account the delay or latency required to bring about the effects of adaptation tactics . In [12], [14], latency-aware adaptation is studied using stochastic multi-player games (SMGs). In [13], SMGs are used to generate optimal adaptation plans for architecture-based self-adaptation. These works exploit PRISM and PRISM-games to solve adaptation problems. So, they have the limitations discussed in Section VI-B.

Several other works [47]–[49] studied the optimization of system configurations. In contrast, this paper focuses on behavior optimization. Several recent proposals explored the application of concepts from control theory [50]–[53] to perform system adaptation. One main difference with respect to these works is that their focus is on the optimization of quantifiable and measurable non-functional goals, such as response time, as opposed to behavior optimization based on functional requirements, the primary focus here.

This paper introduces the OBD framework for the model-based-requirements-driven synthesis of reflex controllers for autonomous systems. The framework introduces a model and a language to describe autonomous systems, their environment and requirements. The semantics of the model is defined in the form of an MDP, which can be solved producing optimal adaptation strategies (reflex controllers) for autonomous systems. In comparison with the general-purpose languages proposed by probabilistic model-checkers, OBD solves two main limitations, namely the Markovian assumption and the implicit-event model. This enables the support of a comprehensive set of software requirements and permits the accurate modeling of the environment in which autonomous systems operate.

Future work consists of extending the framework to support online learning (reinforcement learning) [37]. The study of formal adaptation guarantees and assurances [9], [54]–[56], and optimizing the performance of our framework [57], [58] are other future planned extensions.

This work was supported, in part, by Science Foundation Ireland grant 13/RC/2094 and ERC Advanced Grant 291652.

[1] M. Salehie and L. Tahvildari, “Self-adaptive software: Landscape and research challenges,” ACM Trans. Auton. Adapt. Syst., vol. 4, no. 2, pp. 1–42, 2009.

[2] B. H. C. Cheng, R. D. Lemos, H. Giese, P. Inverardi, J. Magee, J. Andersson, B. Becker, N. Bencomo, Y. Brun, B. Cukic, G. D. M. Serugendo, S. Dustdar, A. Finkelstein, C. Gacek, K. Geihs, V. Grassi, G. Karsai, H. M. Kienle, J. Kramer, M. Litoiu, S. Malek, R. Mirandola, H. a. M¨uller, S. Park, M. Shaw, M. Tichy, M. Tivoli, D. Weyns, J. Whittle, D. Lemos, H. Giese, P. Inverardi, J. Andersson, B. Becker, N. Bencomo, Y. Brun, B. Cukic, G. Di, M. Serugendo, S. Dustdar, A. Finkelstein, C. Gacek, K. Geihs, V. Grassi, G. Karsai, H. M. Kienle, J. Kramer, M. Litoiu, S. Malek, S. Park, M. Shaw, M. Tichy, M. Tivoli, D. Weyns, and J. Whittle, “Software Engineering for Self-Adaptive Systems : A Research Roadmap,” Springer, pp. 1–26, 2009.

[3] R. D. Lemos, H. Giese, H. a. M¨uller, M. Shaw, J. Andersson, L. Baresi, B. Becker, N. Bencomo, Y. Brun, B. Cukic, S. Dustdar, G. Engels, K. Geihs, K. M. Goeschka, V. Grassi, P. Inverardi, G. Karsai, J. Kramer, M. Litoiu, J. Magee, S. Malek, S. Mankovskii, R. Mirandola, J. Mylopoulos, O. Nierstrasz, M. Pezz`e, C. Prehofer, W. Sch¨afer, R. Schlichting, D. B. Smith, J. P. Sousa, G. Tamura, L. Tahvildari, M. Norha, T. Vogel, D. Weyns, K. Wong, and J. Wuttke, “Software Engineering for Self-Adaptive Systems : A Second Research Roadmap,” Softw. Eng. Self-Adaptive Syst., no. October 2010, pp. 1–32, 2011.

[4] N. Esfahani and S. Malek, “Uncertainty in Self-Adaptive Software Systems,” Lect. Notes Comput. Sci., pp. 214–238, 2013.

[5] G. A. Moreno, J. C´amara, D. Garlan, and B. Schmerl, “Proactive self- adaptation under uncertainty: a probabilistic model checking approach,” ESEC/FSE 2015, pp. 1–12, 2015.

[6] A. Van Lamsweerde, Requirements engineering : from system goals to UML models to software specifications. John Wiley, 2009.

[7] P. Zave and M. Jackson, “Four dark corners of requirements engineer- ing,” ACM Trans. Softw. Eng. Methodol., vol. 6, no. 1, pp. 1–30, 1997.

[8] R. Calinescu, L. Grunske, M. Kwiatkowska, R. Mirandola, and G. Tam- burrelli, “Dynamic QoS Management and Optimisation in Service-Based Systems,” TSE, vol. PP, no. 99, p. 1, 2010.

[9] A. Filieri, G. Tamburrelli, and C. Ghezzi, “Supporting Self-Adaptation via Quantitative Verification and Sensitivity Analysis at Run Time,” IEEE Trans. Softw. Eng., vol. 42, no. 1, pp. 75–99, 2016.

[10] J. Kephart and D. Chess, “The vision of autonomic computing,” Computer (Long. Beach. Calif)., no. January, pp. 41–50, 2003.

[11] D. Weyns, “Software Engineering of Self-Adaptive Systems: An Organ- ised Tour and Future Challenges,” Handb. Softw. Eng., pp. 1–41, 2017.

[12] J. C´amara, G. A. Moreno, and D. Garlan, “Stochastic game analysis and latency awareness for proactive self-adaptation,” SEAMS, no. June, pp. 155–164, 2014.

[13] J. C´amara, D. Garlan, B. Schmerl, and A. Pandey, “Optimal planning for architecture-based self-adaptation via model checking of stochastic games,” Symp. Appl. Comput., pp. 428–435, 2015.

[14] J. C´amara, G. A. Moreno, D. Garlan, and B. Schmerl, “Analyzing Latency-Aware Self-Adaptation Using Stochastic Games and Simulations,” ACM Trans. Auton. Adapt. Syst., vol. 10, no. 4, pp. 1–28, 2016.

[15] M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of Probabilistic Real-Time Systems,” in Int. Conf. Comput. Aided Verif., 2011, pp. 585–591.

[16] F. Bacchus, C. Boutilier, and A. Grove, “Rewarding Behaviors,” in Thirteen. Natl. Conf. Artif. Intell., 1996, pp. 1160–1167.

[17] C. Boutilier, T. Dean, and S. Hanks, “Decision-Theoretic Planning: Structural Assumptions and Computational Leverage,” J. Artif. Intell. Res., vol. 11, pp. 1–94, 1999.

[18] P. Sawyer, N. Bencomo, J. Whittle, E. Letie, and A. Finkelstein, “Requirements-aware systems: A research agenda for RE for self-adaptive systems,” RE, pp. 95–103, 2010.

[19] J. Whittle, P. Sawyer, N. Bencomo, B. H. Cheng, and J. M. Bruel, “RELAX: A language to address uncertainty in self-adaptive systems requirement,” Requir. Eng., vol. 15, no. 2, pp. 177–196, 2010.

[20] M. Morandini, L. Penserini, A. Perini, and A. Marchetto, “Engineering requirements for adaptive systems,” Requir. Eng., vol. 22, no. 1, pp. 77–103, 2017.

[21] H. Skubch, “Modelling and Controlling Behaviour of Cooperative Au- tonomous Mobile Robots,” Ph.D. dissertation, 2012.

[22] R. E. Fikes and N. J. Nilsson, “STRIPS : A new approach to the Application of theorem proving to problem solving,” vol. 2, no. October, pp. 189–208, 1971.

[23] D. Mcdermott, M. Ghallab, A. Howe, C. Knoblock, A. Ram, M. Veloso, D. Weld, and D. Wilkins, “PDDL - The Planning Domain Definition Language,” CVC TR-98-003/DCS TR-1165, Yale Center for Computational Vision and Control, Tech. Rep., 1998.

[24] E. Letier and A. Van Lamsweerde, “Deriving operational software specifications from system goals,” ACM SIGSOFT Softw. Eng. Notes, vol. 27, no. 6, p. 119, 2002.

[25] Mausam and A. Kolobov, Planning with Markov Decision Processes: An AI Perspective, 2012, vol. 6, no. 1.

[26] M. L. Littman, T. L. Dean, and L. P. Kaelbling, “On the Complexity of Solving Markov Decision Problems,” Uncertain. Artif. Intell., pp. 394– 402, 1995.

[27] F. Bacchus, C. Boutilier, and A. Grove, “Structured solution methods for non-Markovian decision processes,” AAAI, pp. 112–117, 1997.

[28] M. Cashmore, M. Fox, D. Long, D. Magazzeni, B. Ridder, A. Carrera, N. Palomeras, N. Hurtos, and M. Carreras, “Rosplan: Planning in the robot operating system.” in ICAPS, 2015, pp. 333–341.

[29] J. Sun, Y. Liu, J. S. Dong, and J. Pang, “Pat: Towards flexible verification under fairness,” ser. Lecture Notes in Computer Science, vol. 5643. Springer, 2009, pp. 709–714.

[30] C. Dehnert, S. Junges, J.-P. Katoen, and M. Volk, “A Storm is Coming: A Modern Probabilistic Model Checker,” in Comput. Aided Verif., 2017, vol. 10427, pp. 592–600.

[31] “PDDL4J library.” [Online]. Available: https://github.com/pellierd/ pddl4j

[32] F. Heidenreich, J. Johannes, S. Karol, M. Seifert, and C. Wende, “Model- Based Language Engineering with EMFText,” 2013, pp. 322–345.

[33] R. S. Iadine Chades, Guillaume Chapron, Marie-Josee Cros, Frederick Garcia, “Markov Decision Processes Toolbox,” 2017.

[34] J. Ellson, E. Gansner, L. Koutsofios, S. C. North, and G. Woodhull, “Graphviz - Open Source Graph Drawing Tools,” 2002, pp. 483–484.

[35] I. Epifani, C. Ghezzi, R. Mirandola, and G. Tamburrelli, “Model Evolution by Run-Time Parameter Adaptation,” Proc. - Int. Conf. Softw. Eng., pp. 111–121, 2009.

[36] R. Calinescu, Y. Rafiq, K. Johnson, and M. E. Bakr, “Adaptive model learning for continual verification of non-functional properties,” Proc. 5th ACM/SPEC Int. Conf. Perform. Eng. - ICPE ’14, no. May, pp. 87– 98, 2014.

[37] G. Tesauro, “Reinforcement learning in autonomic computing: A man- ifesto and case studies,” IEEE Internet Computing, vol. 11, 2007.

[38] A. Lapouchnian, “Goal-oriented requirements engineering: An overview of the current research,” Tech. Rep. 3, 2005.

[39] A. V. Lamsweerde, Requirements Engineering: From System Goals to UML Models to Software Specifications, 10th ed. Chichester, UK: John Wiley & Sons, 2009.

[40] E. Yu, “Modelling strategic relationships for process reengineering,” Ph.D. dissertation, University of Toronto, 2011.

[41] L. Baresi, L. Pasquale, and P. Spoletini, “Fuzzy goals for requirements- driven adaptation,” RE, pp. 125–134, 2010.

[42] A. Cailliau and A. Van Lamsweerde, “Runtime Monitoring and Resolu- tion of Probabilistic Obstacles to System Goals,” Int. Symp. Softw. Eng. Adapt. Self-Managing Syst., pp. 1–11, 2017.

[43] D. Garlan, S.-W. Cheng, A.-C. Huang, B. Schmerl, and P. Steenkiste, “Rainbow: Architecture- Based Self-Adaptation with Reusable Infrastructure,” Computer (Long. Beach. Calif)., pp. 46–54, 2004.

[44] S. W. Cheng and D. Garlan, “Stitch: A language for architecture-based self-adaptation,” J. Syst. Softw., vol. 85, no. 12, pp. 2860–2875, 2012.

[45] A. Filieri, C. Ghezzi, and G. Tamburrelli, “A formal approach to adaptive software: Continuous assurance of non-functional requirements,” Form. Asp. Comput., vol. 24, no. 2, pp. 163–186, 2012.

[46] M. U. Iftikhar and D. Weyns, “ActivFORMS: active formal models for self-adaptation,” Proc. 9th Int. Symp. Softw. Eng. Adapt. Self-Managing Syst. - SEAMS 2014, pp. 125–134, 2014.

[47] N. Esfahani, E. Kouroshfar, and S. Malek, “Taming uncertainty in self- adaptive software,” FSE, pp. 234–244, 2011.

[48] A. Elkhodary, N. Esfahani, and S. Malek, “FUSION : A Framework for Engineering Self-Tuning Self-Adaptive Software Systems,” FSE, pp. 7– 16, 2010.

[49] N. Bencomo and A. Belaggoun, “Supporting decision-making for self- adaptive systems: From goal models to dynamic decision networks,” REFSQ, vol. 7830 LNCS, pp. 221–236, 2013.

[50] A. Filieri, H. Hoffmann, and M. Maggio, “Automated design of self- adaptive software with control-theoretical formal guarantees,” in Proc. 36th Int. Conf. Softw. Eng. - ICSE 2014. New York, New York, USA: ACM Press, 2014, pp. 299–310.

[51] ——, “Automated multi-objective control for self-adaptive software design,” ESEC/FSE 2015, pp. 13–24, 2015.

[52] S. Shevtsov and D. Weyns, “Keep it SIMPLEX: satisfying multiple goals with guarantees in control-based self-adaptive systems,” FSE, pp. 229– 241, 2016.

[53] A. Filieri, M. Maggio, K. Angelopoulos, N. D’Ippolito, I. Gerostathopoulos, A. B. Hempel, H. Hoffmann, P. Jamshidi, E. Kalyvianaki, C. Klein, F. Krikava, S. Misailovic, A. V. Papadopoulos, S. Ray, A. M. Sharifloo, S. Shevtsov, M. Ujma, and T. Vogel, “Control strategies for self-adaptive software systems,” ACM Trans. Auton. Adapt. Syst., vol. 11, no. 4, 2017.

[54] R. Calinescu, D. Weyns, S. Gerasimou, M. U. Iftikhar, I. Habli, and T. Kelly, “Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases,” IEEE Trans. Softw. Eng., pp. 1–29, 2017.

[55] D. Weyns, N. Bencomo, R. Calinescu, J. C´amara, C. Ghezzi, V. Grassi, L. Grunske, P. Inverardi, J.-M. Jezequel, S. Malek, R. Mirandola, M. Mori, and G. Tambrrellii, “Perpetual Assurances for Self-Adaptive Systems,” Softw. Eng. Self-Adaptive Syst. 3, no. 9640, 2017.

[56] M. U. Iftikhar and D. Weyns, “ActivFORMS: A runtime environment for architecture-based adaptation with guarantees,” Softw. Archit. Work., pp. 278–281, 2017.

[57] A. Pandey, G. Moreno, J. C´amara, and D. Garlan, “Hybrid Planning for Decision Making in Self-Adaptive Systems,” 10th IEEE Int. Conf. Self-Adaptive Self-Organizing Syst. (SASO 2016), 2016.

[58] G. A. Moreno, J. Camara, D. Garlan, and B. Schmerl, “Efficient decision-making under uncertainty for proactive self-adaptation,” Proc. - 2016 IEEE Int. Conf. Auton. Comput. ICAC 2016, pp. 147–156, 2016.

This appendix presents formally the mapping of OBD model descriptions into an MDP.

A model description is a tuple , an is the MDP built on the basis of if its various elements are constructed as described below.

State Atoms: Let be the set of state variables of and be their corresponding domains. An assignment of a value to a state variable is called a state atom over . The set of state atoms and is called the set of state atoms of .

Requirement Variables and Requirement Atoms: Let RQ be the requirements of . Let be a requirement and name(r), type(r) and states(r) be functions returning the requirement’s identifier, type and its possible states respectively. For example, let r = ReqID m achieve S if A unless Z reward r. In this case, name(r) = m, type(r) = CA and states(r) = {I, R}. The set of requirements variables of is the set such that every is the name of a different requirement in RQ. The domain of every is its set of possible states, i.e., . The set and is called the set of requirement atoms of .

Definition 1 (States S): Let V be the set . In this case, the set of states generated from V is the set S = .

Intuitively, the previous definition means that every state S is a set of atoms such that a value is assigned to every variable . A state s includes both state and requirements atoms. We distinguish between them as follows: state atoms of a state s are referred to as the base state of s, denoted s, and requirement atoms are referred to as the expanded state of s, denoted . More formally, let s be a state, , whereas . This distinction is needed as state and requirements are updated differently: state atoms are directly updated by occurrence of actions and events; on the other hand, requirements atoms are indirectly updated if their status need be updated as a result of change in state atoms.

Action Representation: Let an action expression AV be a tuple where a is the action name, cost its cost, is one of its preconditions, every is one effect x of the execution of a when the precondition holds and is the probability of producing the effect x.

Definition 2 (Actions): The set of actions A is the set of action names in AV and the noop action, i.e., A is where noop is an action which execution has no cost and produces no effects.

Formula Satisfaction: Let f be a formula of the form 6 and Y a set of atoms. The satisfaction of a formula f in Y , denoted Y |= f, is defined in the usual way as follows:

be the action description of in . The execution of a in s produces a state r with a probability p iff:

• a precondition of the action description ad is satis-

– its base state is s after the update of the value of every state variable in which appears in with the value specified in . Formally, this is represented as follows: where ,

– its expanded state is after the update of the state of every requirement according the state transition models shown in Fig. (8)(9)(15). Formally, and type(m) = T} where defines how the requirement m of type T should be updated when its current state is st and the newly computed base state is x. This function is defined for every type of requirements according to its state transition model. For example, consider PM requirements of the form ReqId m maintain S for P if A unless Z reward r, the definition of is as follows:

Other functions are similarly defined to describe the update of the state of the other types of requirements as shown in the transitions part of Fig. (8)(9)(15). We define similarly the execution of an event e in a state s as follows.

be the event description ev of an event e in . The execution of e in s produces a state r with a probability p iff:

– its base state is s after the update of the value of every state variable in which appears in with the value specified in . Formally, this is represented as follows: where , – its expanded state is after the update of the state of every requirement according the state transition models shown in Fig. (8)(9)(15). Formally, and type(m) = T} where defines how the requirement m of type T should be updated when its current state is st and the newly computed base state is x due to an event occurrence. The function is defined similarly to with the exception that events do not cause time-related transitions in the requirements’ state machines since they occur concurrently with actions. For example, consider PM requirements of the form ReqId m maintain S for P if A unless Z reward r, the definition of is as follows:

be an event description ed of an event e in . The occurrence vector of e is a vector of length |S| whose entries are defined as follows:

Explicit Action Transition Matrix: Let be an action and S be the set states. The explicit transition matrix of a, denoted , is a matrix. If the execution of a in a state produces the state with a probability p, then .

Explicit Event Transition Matrix: Let e be an event and S be the set states. The explicit transition matrix of e, denoted , is a matrix. If the execution of e in a state produces the state with a probability p, then .

Effective Events Transition Matrix: Let be the explicit event transition matrices of events in and be their corresponding occurrence vectors. Let be the diagonal matrices with entries and respectively. The effective transition matrix of an event , denoted , is computed as follows:

Given the effective transition matrices of the events , the effective events transition matrix, denoted is computed as follows:

Definition 3 (Action Transition Matrix): Let be the explicit action transition matrices of actions in and be the effective events transition matrix. The (implicit-event) action transition matrix of an action , denoted , is computed as follows:

Definition 4 (Action Reward matrix): Let be an action and S be the set states. The action reward matrix of a, denoted , is a matrix such that if and are states in S, then represents the rewards that are obtained on the transition from the state to minus the cost of the action a. This is expressed as follows: where and (m = and . The function is defined for every requirement according to its type as shown in the rewards part of Fig. (8)(9)(15). For example, consider a PM requirements of the form ReqId m maintain S for P if A unless Z reward r, the definition of is as follows:

Reward functions for the other types of requirements are similarly defined.

Definition 5 (The discount factor): The discount factor is a value between zero and one, i.e., .

The discount factor ensures the convergence of the infinite reward series when computing the total expected rewards. It determines how far into the future the satisfaction of requirements affects the computation of optimal strategies. For example, if be 0.98 and r is the reward defined for requirement m. In this case, the actual reward values obtained if this requirement is satisfied after 50, 100 and 150 time steps are 0.364r, 0.1326r and 0.0482r respectively. The discount factor is therefore chosen according to the requirements of the application domain.

Fig. 15. Duration Requirements: Transitions and rewards