RV 2005 Preliminary Version Steering of Discrete Event Systems: Control Theory Approach

Runtime verification involves monitoring the system at runtime to check for conformance of the execution trace to user defined safety properties. Typically, run-time verifiers do not assume a system model and hence cannot predict violations until they occur. This limits the practical applicability of runtime verification. Steering is the process of predicting the occurrence of violations and preventing them by controlling system execution. Steerers can achieve this using a limited knowledge of the system model even in situations where it is infeasible to store the entire model. In this paper, we explore a control-theoretic view of steering for discrete event systems. We introduce an architecture for steering and also describe different steering paradigms.


Introduction
Verification and validation are established techniques to ensure correctness of software systems. But, verification checks the specification rather than the implementation and validation does not provide guarantees for conformance. Also, verification and validation do not scale well to large systems. Runtime verification checks for conformance of execution traces to formally specified safety properties and hence exports the advantages of verification techniques to trace validation. Although runtime verifiers can efficiently detect nonconformance, they cannot predict violations in advance because they do not have information on the system model. Since any run-time technique deals with a single execution trace, limited knowledge (local to the execution trace) of the system model will be sufficient to predict violations with high confidence. Steering exploits this limited system knowledge to predict violations.
A steerer looks ahead into a partial system model to explore the state space in advance. It then invokes the runtime verifier to detect non conformance and generates control actions to prevent the system from reaching a violation. Steering can thus be defined as the process of analysis (using look ahead) of a partial system model to detect non-conformance (prediction) and application of control actions to the model (prevention). We assume, the steerer and the system to be residing on different machines and executing concurrently. This leads to communication delay in the transmission of event notifications and steering actions between the steerer and the system.
In this paper, we formulate the problem of steering of Discrete Event Systems (DES) as a supervisory control problem. Communication delay is accounted for by assuming partial observability of the system. We introduce a generic architecture for steering and propose four different steering paradigms. Constraints imposed on the system model and the steering overhead to the system are used to classify these paradigms. The paper then describes a subway system example to which a particular paradigm is applied.
Related Work: Stephane et. al. in their online control work [3], [4], [6] present a control-theory-based approach for control of DES with limited look ahead. We adapt this work to the steering problem where steerers must generate control actions with as little latency as possible in the presence of communication delays and concurrent execution. The steering framework described in [8], [10] is specific to a particular runtime verifier and assumes that a recovery after the occurrence of a violation is always possible. It assumes no knowledge of the system model and hence the user is required to specify steering actions. Papers [5], [7], [1] provide very domain specific solutions to simpler control problems and would be extremely inefficient in a general framework.
The rest of the paper is organized as follows. Section 2 lists motivating examples for steering and Section 3 formally defines the steering problem. Section 4 introduces the steering architecture and Section 5 formulates the steering problem as a control problem under partial observability. Section 6 describes four steering paradigms and Section 7 gives an illustrative example. Section 8 concludes the paper and indicates future research directions.

Motivation
When developing a software system, the designer and the users have at least an informal idea of properties that the system must satisfy. However, subtle errors throughout the software engineering process can lead to an incorrect implementation. Static analysis of an abstract model of the implementation to eliminate undesirable behaviors is a challenging problem when the state space  to be explored is large or time varying(dependent on external environment). Thus, in order to eliminate undesirable behaviors while preserving a rich set of allowable behaviors, we must use dynamic control. In this section, we list a few examples from different domains that support our claim for the need of a steerer.

Scheduling of real-time tasks using actual execution time
The paper [1] introduces a real-time task model in which the worst case execution times for each task, minimum and maximum execution periods for each task and the desired system utilization are given. The runtime verifier monitors task executions to determine their actual execution times and then evaluates the actual utilization of the system. The steerer uses this utilization estimate to adjust task periods so that the desired utilization may be achieved. This architecture is shown in Figure 1(a).

Reconciling System Requirements at run-time
At run-time, a software system can deviate from its expected behavior because of changes in the system environment. The paper [5] suggests two approaches for runtime steering. As shown in Figure 1(b), steering can be achieved by monitoring the system and modifying control parameters to minimize deviations. If the deviation is large, the steerer could also request that an alternate design model be used by the system. For example, consider a meeting scheduler scheduling a meeting based on the availability times of all the participants. One of the system requirements is that the scheduler should be able to get the availability times of the participants. One way of achieving this goal is by locating the agenda for each participant and extracting the availability times.
An alternate approach would be to send email requests to participants. Steering would then involve switching between these approaches depending on the accessibility of the agenda. When using the email model, the steerer can also monitor the delay in response of participants and adjust reminder frequencies accordingly.

Inverted Pendulum
Paper [8] describes a control system which consists of an inverted pendulum run by an experimental controller. The experimental controller generates random values for the motor speed of the pendulum. The runtime monitor checks if the experimental controller is maintaining the pendulum within a stable region. If the monitor detects a violation it switches the control to a safety controller which maintains the pendulum in the stable region. This experiment demonstrates the use of steering in a continuous-variable, constrained environment.

Problem Statement
As described in Section 2 steering is essential to detect certain errors in software, especially when the system state space is large or time varying. In this paper, we develop a steering architecture and steering paradigms for DES with large state spaces.

Steering for DES with large state spaces
Any steerer for a DES must satisfy the following properties, Light Weight: Steering must be light weight i.e., the steerer should not behave like a central controller.
Fast: Low response time is desirable because steering actions are state dependent. Low response time is also a desired property when steering realtime systems.
Minimally restrictive: Steering must restrict the system model minimally while ensuring that violations do not occur.
We now formulate the steering problem for DES with large state spaces. A DES is a transition system M = S, T, Σ , where S is the large state space, Σ is the event set and T is the transition function T : S × Σ −→ S. We assume that all the events Σ are controllable by the steerer. The state space S is discrete and hence finite or countably infinite. The state machine is event driven i.e., at each time instant at most one event can be generated. Let, n be the round-trip communication delay between the system and the steerer. This means that the system can generate a maximum of n events between the generation of an event e and the reception of steering action corresponding to e. We assume that the processing delay of the steerer is negligible compared to this delay. The steering problem can then be decomposed into the following problems: Given communication delay n, current state s 0 of the DES M and the system model M , (i) Predict non-conformance to user defined safety properties along different execution paths originating from s 0 in the partial system model (ii) Generate appropriate steering actions to ensure that the system does not reach violation by restricting the partial model (iii) Determine a steering paradigm for execution of the steering actions by the system Problem (i) can be formulated as a standard runtime verification problem once the partial system model has been generated. Problem (ii) has been addressed in this paper using supervisory control theory for DES. Steering paradigms designed later in the paper provide a solution to problem (iii). The same architecture and paradigms can be used for time varying systems if the partial system model for such systems can be generated at each step.

Steering Architecture for DES
The communication delay between the system and the steerer dictates the minimum amount of look ahead that the steerer must use to ensure that steering actions are transmitted to the system in time. Further, since steering actions are state dependent, each action must be executed by the system at the state for which that action was generated. In this section, we develop a steering architecture for DES which addresses these issues.

Steering Architecture
In response to an event notification, the steerer must generate a partial (n + 1) step DES originating from the current state as shown in Figure 2. n + 1 is the minimum amount of look ahead required to ensure that steering actions are received by the system in time. The states of this DES are known as runtime states and each state uniquely identifies an execution trace in the system. Formally, the runtime DES for a current state s 0 and system model M can be defined as G s 0 = S , R, Σ, s 0 , F, C, T . S is the set of runtime states and R defines a function, mapping runtime states in S to static states S in DES M . s 0 ∈ S is the initial state of G s 0 and Σ is the event set. T : where e ∈ Σ. F ⊂ S is the set of final states of the runtime DES and C ⊂ S is the set of control states defined as C = {s ∈ S |∃e ∈ Σ, f ∈ F, T (s , e) = f }. The steering action for s 0 will disable some of the transitions with source states in C.
In response to a request from the steerer, the runtime verifier finds a set of violating states F such that F ⊆ F . Let, G s 0 be the steered system for the original system G s 0 such that F is not reachable in G s 0 . Some steering paradigms might require that the steerer send activation and deactivation signals to the system for each steering action. These signals occur at points in the execution of the system and the steering action is applicable in the interval  of time between these points. These signals are necessary because there is no synchronization between the system and the steerer and steering actions are associated with specific system states. An activation signal is of the form A, N, Σ d , Σ e where A implies activation and N is the action number. The steerer uses this number(unique for every activation-deactivation pair) when sending the deactivation signal. Σ d is the set of events to be disabled and Σ e is the set of events to be enabled in the system model. The deactivation signal is of the form D, N where D implies deactivation.
The architecture of a DES with a steerer and a runtime verifier is shown in Figure 3. The functions of each of the modules in the architecture is described below.
• System(DES): When an event is generated, the system sends an event notification to the steerer. On receipt of a steering action, the system may either apply the action immediately or store it for future use depending on the steering paradigm employed. The system may also receive activation and deactivation signals from the steerer. When the system receives an activation signal, it executes the accompanying steering action. When it receives a deactivation signal, it deactivates the action corresponding to the action number accompanying the signal.
• Steerer: On receiving an event notification from the system, the steerer generates the partial runtime DES G s 0 . It then sends the set of final states F in G s 0 to the runtime verifier. For each state u ∈ C having transitions to F , the steerer generates the set Σ u d of events that need to be disabled(transitions leading to F ). The steering action for the state s 0 is then given by Similarly, the steerer could also generate a set of enabled events Σ e for C depending on the paradigm. • generating steering actions for G s 0 . This would involve determining the violating states in G s 0 using the runtime verifier and • determining a steering paradigm for the execution of steering actions.
Given system model M , current state s 0 and the steered runtime DES G s 0 from the previous iteration, the steerer can efficiently compute the new runtime DES G s 0 . If e ∈ Σ is the current event received from the system, the steerer updates its runtime state to s 0 = T (s 0 , e) where T is the transition relation in G s 0 . It then computes the states f ∈ F \ F of G s 0 that are reachable from s 0 . G s 0 is now generated by determining the successor states of this reachable set using M .

Control Theory based Steering
The runtime DES G s 0 for which we wish to generate steering actions is a finite state machine. This steering problem can be formulated as a static control problem for DES under partial observation. The partial observation is as a result of the fact that the steerer has limited knowledge of the current state of the system due to communication delay.

Steering of runtime DES as a Static Control Problem
Let, G be the finite DES for which we wish to design a controller and M = L(G) denote the language generated by G.L(G) = {s ∈ Σ * : (∃t ∈ Σ * ) ∧ (st ∈ L(G))} is the prefix closure of L(G). Let, S denote the finite DES(supervisor) we wish to design such that L(S × G) ⊆ L(G) where L(S × G) is the language generated by the supervised system. Σ o ⊆ Σ denotes the set of observable events and Σ u = Σ \ Σ o denotes the set of unobservable events. P is a projection function defined on event strings denoted as P : Σ * −→ Σ * o . Figure 4 shows the architecture for control of finite DES under partial observation. The supervisor S can be defined by a function SC : P (L(S × G)) −→ 2 Σ given by s ∈ L(S × G) ∧ sσ ∈ L(G) ∧ σ ∈ SC(P (s)) ⇒ sσ ∈ L(S × G). Two different strings can be equivalent under partial observation and hence the control actions required for these two strings in order to generate the controlled language must be the same. The observability condition is used to determine whether a controlled language is admissible for a given system under given partial observability. Let, where N ⊆ Σ * . Basically, supP (N ) is given by the set {s|(s ∈ N ) ∧ (All pref ixes of s are in N )}. Let K be any language such that K ⊆ L(G) and K = φ. We wish to decide if we can design a supervised system S generating K(K = L(S × G)) and admissible for M under the projection P . The observability condition given in [2] can be stated as, K is said to be observable with respect to M and P if The observability condition given in [9] can be defined as, K is observable with respect to M and P if and only if supP (P i (K)) ∩ M ⊆K Proof of equivalence of these two observability conditions is given in Appendix A. Steering paradigms described later in the paper will restrain the system model using these observability conditions to ensure correctness of the paradigm. Generation of steering actions for the runtime DES G s 0 can now be formulated as a static control problem under partial observation. G s 0 is the finite DES for which we wish to design a steerer and G s 0 denotes the steered DES. The steering problem can now be stated as, Given G s 0 and the set F ⊆ F of violating states, design G s 0 such that F is not reachable in the controlled system G s 0 . G s 0 and G s 0 must satisfy observability conditions specified in the particular steering paradigm used.

Steering Paradigms
In this section we describe different steering paradigms that can be adopted under the architecture defined in Section 4. Since the steerer and the system have inconsistent views of the current state of the system, the steerer must assist the system in determining the state at which a particular steering action must be executed.

Paradigm 1: Unconstrained System Model(Hashing based Steering)
Steering paradigms under this classification do not impose any restrictions on the system model. Hashing based execution of steering actions is one such paradigm. In this approach, the steerer sends hashed values of event strings(states u in C that have transitions to violating states in F ) and the corresponding set of disabled events(Σ u d ) to the system. The system stores these values in a hash table. When an event occurs, the system generates a new hash value(incrementally) for the event string seen so far and hashes into this table. On a hit, the system activates the steering action associated with that slot. This action can be deactivated on the occurrence of any further event.
We now design a hash function for this paradigm. Let, (k − 1) denote the number of different events in the system model. We will then use a radix-k representation for event strings. Each event e ∈ Σ will be associated with a unique integer i e ∈ (1, k − 1). For every event string es = e 1 e 2 · · · e l where i e 1 , i e 2 , · · · , i e l are the unique integers for events e 1 , e 2 , · · · , e l respectively, its radix-k representation r es = i e l + i e l−1 × k + · · · + i e 1 × k l−1 . Given es and its radix-k representation r es , the radix-k representation of the event string es = es.e l+1 (. represents string append) is r es = i e l+1 + (r es × k).
This representation splits event strings into different ranges of natural numbers depending on string lengths. The hash function we design, will ensure that event strings with different lengths do not hash into the same slot. We split the entire hash table into n regions numbered 0, · · · , (n − 1) each of the same size. Event string es ∈ Σ * will hash into the (|es| mod n) th region in the hash table where |es| denotes the string length. Splitting the hash table into n regions is sufficient because n is the communication delay. When steering action for a string of length 2n is received by the system, the system must have executed the action for strings of length n(steerer generates steering actions for strings of length 2n after the system reaches states corresponding to strings of length n). All strings of length less than n cannot be associated with any steering action and hence will hash into a single slot.
Let, m + 1 be the total size of the hash table where m/n is an integer. The size of each region is m/n and slot 0 will be used to hash all strings of length less than n. The hash function is then given by, h(r es , i) = 0 i ≤ (n − 1) = (r es mod m/n) + ((i mod n)(m/n)) + 1 otherwise The relation between r es and i in the hash function is given by (k i − 1)/(k − 1) ≤ r es ≤ (k i − 1). The average chain length at each slot is α = O(((k − 1) n )n/m) because the maximum number of strings that can hash into a single region is always (k − 1) n (steerer generates steering actions for runtime states in C using G s 0 and has complete knowledge of the execution trace upto s 0 . The length of any event string originating from s 0 and terminating in some state in C is always n).
Splitting the hash table into n regions up front can lead to under utilization of the hash table. The modified hash function which splits the hash table dynamically is given by, h(r es , i, j) = 0 i ≤ (n − 1) = (r es mod m/j) + ((i mod n)(m/j)) + 1 otherwise The steerer will now send the entire hash table to the system every time it generates new steering actions. In practice, violating states are a small subset of the state space and hence the number of entries in the hash table will be small. The steerer also sends the number of regions j into which the hash table is currently split. Advantages This paradigm does not impose any restrictions on the system model. Disadvantages There is an overhead on the system for storing the hash table and for computing the hash function.

System correctness
System correctness depends on the interaction between event strings that participate in a collision in the hash table. A conflict occurs between two colliding strings only when an event disabled by the steering action of one string is required to be enabled in the other. We make a pessimistic assumption that two colliding strings lead to incorrect control when either of them have any steering action associated with them. Let, h denote the number of hash slots in each region of the hash table, p the average number of strings hashing into a region and d the average number of strings that have steering actions associated with them. Let the set of event strings that have steering actions associated be denoted by D. Assuming simple uniform hashing, the probability of collision between any two strings r es1 , r es2 hashing into the same region and having same length i is P rob{h(r es1 , i) = h(r es2 , i)} = 1/h. The probability that the system during its execution generates one of the strings from r es1 and r es2 is P rob{ System generates r es1 ∨ r es2 } = 2/p. Using our assumption, the probability that r es1 and r es2 conflict is given by, Given n is the number of regions in the hash table and P rob{Region f ails} is the probability of failure(colliding and conflicting strings) in one region, the probability that the steered system is correct is, P rob{System correct} = [1 − P rob{Region f ails}] n Now, P rob{Region f ails} = P rob{h(r es1 , i) = h(r es2 , i)} × P rob{ System generates r es1 ∨ r es2 } × P rob{r es1 , r es2 conflict } = 1/h × 2/p × [P rob{r es1 , r es2 conflict |r es1 ∈ D or r es2 ∈ D}× P rob{r es1 ∈ D or r es2 ∈ D}+P rob{r es1 , r es2 conflict |r es1 ∈ D and r es2 ∈ D}× P rob{r es1 ∈ D and r es2 ∈ D}] Therefore, P rob{Region f ails}

Constrained System Model
In this steering paradigm we reduce the steering overhead on the system by constraining the system model. A constrained model will provide opportunities for automated activation and deactivation of steering actions. Let, P n 1 ,n 2 (s) = s.s such that n 1 ≤ |s | ≤ n 2 where s, s ∈ Σ * and |s | denotes length of string s . Also, let G s 0 be the original system, F be the final states of G s 0 and G s 0 be the steered system.

Paradigm 2: Event Trace based Steering
In this approach, the steerer sends the disabled event set Σ d and its observed event trace s 0 to the system. The system compares its own event trace with the trace sent by the steerer and determines the distance to C(states where steering actions must be executed) for that steering action. It stores this distance along with the steering action and decrements the distance at the occurance of each event. When this distance reduces to zero, the corresponding steering action is executed. Deactivation can be done at the occurance of any further event. When the steering action is executed, the system could be in any state in C. To ensure correctness, the system model must satisfy the observability condition given in Section 5.1 whereK = G s 0 , M = G s 0 and all strings in G s 0 are equivalent under projection P . Advantages This paradigm imposes less overhead on the system as compared to hashing.
Disadvantages The system must store its event trace and also update the distance metric for all the stored steering actions at the occurance of every event. The system model is also constrained by the observability condition.

Paradigm 3: Steering with Observability Condition and Minimum Separation
In this paradigm, the system will disable all the events in Σ d as soon as it receives the steering action A, N, E d , E e (N not required). To ensure admissibility of the steering action, the system model must satisfy the observability condition as in paradigm 2. The system will deactivate the steering action as soon as any event in Σ d ∪Σ e occurs. A minimum separation property of events in the model will ensure correctness of this deactivation procedure. Minimum separation is given by, This property ensures that no event in Σ d ∪ Σ e will occur in any of the transitions with source states in S \ (F ∪ C).
Advantages Event traces are not required to be stored by the system in this paradigm. The steering overhead on the system is also minimal.
Disadvantages The steerer is required to send both the event sets Σ d and Σ e . The system model is also severely constrained.

Paradigm 4: Steering with Stringent Observability Condition
In this approach, the system will disable all the events in Σ d as soon as it receives the steering action A, N, Σ d , Σ e (Σ e is empty). When the steerer sends the activation signal, it stores the action number N alongwith the corresponding set of final states F of G s 0 . When the steerer receives an event notification, it checks if the current state matches with any state in F for any action number. If such a match occurs for action number N , the steerer sends the deactivation signal D, N . On receiving a deactivation signal, the system deactivates the steering action specified by the action number. To ensure admissibility of steering actions, the system model must satisfy a modified observability condition given by, s 0 is the steered runtime DES originating from s 0 and having depth 2n + 1. When the system receives the activation signal, it could be in any of the states in S \ F and when it receives the deactivation signal it could be in any state which is at a distance of atmost n steps from some state in F . The modified observability condition ensures that if σ ∈ Σ d , then all the σ transitions in this entire region are disabled.
Advantages This paradigm induces minimal steering overhead on the system. The restriction on the system model is less stringent than in paradigm 3.
Disadvantages The steerer has to send deactivation signals and also needs additional storage for previously sent activation signals.

Illustrative Example
In this section, we apply steering paradigm 4 to an example of a simple subway system [3]. We demonstrate the ability of our architecture to prevent the subway system from entering violations and highlight the constraints that the steering paradigm enforces on the system model.

Simple Subway System
As shown in Figure 5, a subway system consists of stations, junctions, trains and a set of tracks with directions. Each train is represented by its source station, destination station and a route. We assume each track is further divided into 4 sections. This is a good example for dynamic control because the state space grows with the number of trains in the system and this in general can be very large. Safety properties for this subway system may include, (i) Limit on the maximum number of trains at any given time at any junction. For example, let one safety property be "Junction J1 has capacity for only 2 trains at any given time" (ii) Balanced usage of tracks in the system. For example, let the system be constrained by the property that "The difference in loads(number of trains that have used the track) in tracks T6 and T7 must never exceed 4".
We would like to steer the system and prevent it from violating any of these safety properties. We assume that the round-trip communication delay between the steerer and the subway system is n = 1.

Steering of Subway System
Let, α(i, j, k) represent the event that train k enters section j of track i and α(i, 5, k) represent the event that train k left track i and entered a junction or a station. Let for example, the system consist of three trains X, Y and Z. Assume train X executed event α(1, 4, X) and Y executed event α(2, 4, Y ) most recently. Let train Z be currently at junction J1 and let s represent this state of the combined system. At this state, the system can violate safety property 1 in n + 1 = 2 steps(both X and Y decide to enter J1 without train Z leaving it). Hence the steerer, under paradigm 4, will disable events α(1, 5, X) and α(2, 5, Y ) at state s as shown in Figure 6. Train Z could move to section 1 of track T 3 before trains X and Y arrive at junction J1 and this will ensure that property 1 is not violated. But for admissibility of the steering action under paradigm 4, the system must satisfy observability condition specified in section 6.2.3. This condition would require that events α(1, 5, X) and α(2, 5, Y ) be disabled in all states which are at most n + 1 = 2 steps from s as shown in Figure 6. If we use hashing based steering(Paradigm Let, β k represent the event that train k enters track T 7 from S2 and γ k be the event that train k enters track T 7 from J2 . Safety property 2 can now be written as −4 ≤ (|β| + |γ| − |α(6, 1, * )|) ≤ 4 where |e| represents the number of occurrences of event e(ignoring train numbers) in the system execution history. Let, the system currently consist of trains A and B only where train A has executed event α(3, 4, A) most recently and train B is at station S2. Also, let the current value of (|β| + |γ| − |α(6, 1, * )|) be −4. Now, if train A enters track T 6 before train B enters track T 7, safety property 2 will be violated. To prevent this, the steerer will disable event α(6, 1, A) at the current state. The observability condition in section 6.2.3 does not block safe states in this case as shown in Figure 7.

Conclusion and Future Work
In this paper, we have introduced an architecture for steering of DES with large state spaces and also described different steering paradigms for execution of steering actions. Runtime monitors equipped with steerers will be able to predict occurrence of violations well in advance to be able to steer the system away from them. The paper, essentially views the steerer as a dynamic controller that uses the runtime verifier as a sub-module to predict violations. If the violations are restricted to a small subset of the state space, then this architecture will provide efficient steering for DES with large state spaces.
Generation of the partial system model for time varying systems is an important extension for this steering architecture. Extending the steering architecture to models where not all transitions are controllable is also a natural area to explore because in a typical system not all execution points are controllable. Reducing steering overhead by using probabilistic prediction of violations is another direction for further work.

A Equivalence of Observability Conditions
The observability condition given in [2] can be stated as, K is said to be observable with respect to M and P if ∀s ∈K ∧ ∀σ ∈ Σ, (sσ ∈K) ∧ (sσ ∈ M ) ⇒ P −1 [P (s)]σ ∩K = φ (A.1) The observability condition given in [9] can be defined as, K is observable with respect to M and P if and only if supP (P i (K)) ∩ M ⊆K (A.2) We first prove some lemmas which will then be used to prove the equiva- Lemma A.2 sσ ∈ P i (s σ) ⇔ s σ ∈ P i (sσ) Proof. We now prove that sσ ∈ P i (s σ) implies s σ ∈ P i (sσ). From the definition of P i (.), sσ ∈ P i (s σ) ⇒ s ∈ P −1 [P (s )] ⇒ s ∈ P −1 [P (s)] ⇒ s σ ∈ P −1 [P (s)]σ ⇒ s σ ∈ P i (sσ).