Model-Based Synthesis of Incremental and Correct Estimators for Discrete Event Systems

1 Introduction

For autonomous systems, state estimation and tracking is a critical task because it strongly influences the decisions that are made and that can be essential to the life of the system. It provides the means to diagnose the faults and to react to the various hazards that can affect the system.

In this paper, we focus on discrete event systems [Zaytoon and Lafortune, 2013]. When the system state is partially observable, the number of candidate estimates can quickly become too large to be usable. In embedded or distributed systems, memory and communication limitations can also become a problem, even with symbolic representations techniques such as in [Torta and Torasso, 2007]. These limitations lead us to propose an estimation strategy that retains only one state out of the set of candidate estimates at each time step, as in [Bouziat et al., 2018]. This can be seen as an extreme strategy but nevertheless efficient to feed the decision system with a clear input and consistent with several works that select a limited number of best candidates according to some preference criterion, for example probabilities like in [Williams and Nayak, 1996;

Kurien and Nayak, 2000]. However, the more we limit the number of estimates, the more we may be confronted with the problem of dead-ends related to the fact that next observations may prove that previous estimates were wrong and there is no continuation in the estimated trajectory. Because backtracking [Kurien and Nayak, 2000] is not a viable solution with real time constraints, we propose to build single-state estimators that are guaranteed to avoid dead-ends. The ability of a system to support the construction of a single-state dead-end free estimator has been defined as single-state trackability in [Bouziat et al., 2019].

Several properties have been investigated for discrete event systems. A system is (strongly) detectable if one can determine its state along some (all) trajectories of the system [Shu et al., 2007]. Diagnosability [Lafortune et al., 2018] and manifestability [Dague et al., 2019] amount to strong detectability and detectability for faulty trajectories. Singlestate trackability is somewhat orthogonal to these properties.

In this paper, we recall the necessary and sufficient condition for single-state trackability as it is derived in [Bouziat et al., 2019] based on equality of regular languages. A first contribution is to show that this condition can be expressed in terms of the simulation relation between automata [Hol´ık et al., 2018]. This allows us to provide a complexity bound for the single-state trackability problem and a way to build estimators endowed with this property. A second contribution of the paper is to propose two customizable correctness criteria that lead the estimator to constrain the acceptable estimator states towards the real states of the system. A third contribution is an implementation that relies on the Sat Modulo Theory (SMT) solver MONOSAT for synthesising estimators. Intensive experiments show that our implementation is able to synthesize dead-end free estimators on real world scenarios.

The paper is organised as follows. Related work is discussed in Section 2. Section 3 introduces incremental singlestate estimation and how it is performed in our framework. The property of single-state trackability is defined and characterized in Section 4 and the associated decision problem is proved to be in NP. Customisable correctness of single-state estimators is formalized in Section 5. Section 6 presents the SMT encoding for synthesizing single-state estimators given a system specification. Experimental results are presented in Section 7, and future work is discussed in Section 8.

2 RelatedWork

A related research domain is the well-known controller synthesis problem, as described in [Ramadge and Wonham, 1987]. Given a specification of the system, controller synthesis consists in finding a decision procedure that produces a command to apply to the system, given observations as input. Under partial observability, a trend of work proposes to synthesize finite-state controllers, which use a size-limited memory to record information related to the past. These were first introduced for POMDP [Meuleau et al., 1999] and shown to be useful for non-deterministic planning [Bonet et al., 2009; Pralet et al., 2010]. Restricting the information recorded from the past is also one important feature of our approach. However, there are several differences compared to our incremental estimation approach. The above works design controllers guaranteed to satisfy some properties related to planning, in particular the evolution of the controlled system must terminate in a goal state. In our estimation framework, we are rather interested in correctness properties, i.e. guaranteeing that the estimated state is "as close as possible" to the real state of the system (see Section 5).

Controller synthesis has also been approached within the game theory framework. In particular, [Doyen and Raskin, 2011] consider observation-based strategies for two-player turn-based games. Similar to our approach, observationbased strategies rely on imperfect information on the past observation sequence, hence defining partially observable games. Such games occur in the synthesis of a controller that does not see the private state of the plant. The main difference with our approach is that game theory considers games as complete graphs. Such a hypothesis means that strategies cannot encounter dead-ends in the execution, i.e. there is always a feasible action from any state of the game.

3 Incremental Single-State Estimation

In this section, we present the process of state estimation for partially observable systems modelled by non-deterministic Moore machines with an empty input alphabet, and whose output alphabet represents the system observations.

Definition 1 (System). A system M is defined by a 5-tuple (S, s0, O, ∆, obs) consisting of the following:

• a finite set of states S;
• an initial state s0 ∈ S;
• a finite set of observations O (output alphabet in the Moore machine);
• a transition relation ∆ ⊆ S2 ;
• an observation function obs : S → O mapping each state to its output.

Without loss of generality, we consider that all the states of the system are reachable from the initial state s0.

We define cands as the function from S × O to 2S such that for all state s in S, for all o in O, cands(s, o) represents the set of successors of s that have observation o. Formally, ∀s ∈ S, ∀o ∈ O, cands(s, o) = {t|(s, t) ∈ ∆ and obs(t) = o}.

We also define nextObs the function S → 2O such that nextObs(s) is the set of observations that can be observed just after the system is in state s. Formally, ∀s ∈ S, nextObs(s) = {o|cands(s, o) ̸= ∅}.

Notation. A state sequence seq is a list (s0, s1, . . . , sn-1) where each si is a state in S; |seq| = n is the length of the sequence and seq[i] = si is the ith state in the sequence; last(seq) designates the last state of seq; if s is a state, seq · s is the sequence of length |seq| + 1 that begins with seq and ends with s. Similarly, we define an observation sequence. We also extend the function obs to a state sequence: if seq is a state sequence, obs(seq) is the observation sequence seqobs such that |seqobs| = |seq| and seqobs[i] = obs(seq[i]) for all i ∈ [0, n - 1].

Definition 2 (Language, observation language). The language associated with a system M = (S, s0,O,∆, obs) is the set of state sequences accepted by the system and starting with s0. Formally L(M) = {seq ∈ S+|seq[0] = s0 and ∀i ∈ [1, |seq| - 1], (seq[i - 1], seq[i]) ∈ ∆}.

The observation language is the language accepted by the system projected on the observations. Formally, Lobs(M) = {obs(seq)|seq ∈ L(M)}.

We now focus on the estimation part for systems defined above. Since we consider non-deterministic, partially observable systems, there may be several state sequences that explain a given observation sequence. We adopt an incremental approach to select a unique explanation, called an estimation strategy. Then, we show that for a given system, any estimation strategy can be represented by a finite state machine called an estimator.

Definition 3 (Estimation strategy). An incremental singlestate estimation strategy for a system M = (S, s0, O, ∆, obs) is a function estim : S × O → S such that for all s in S, for all o in nextObs(s), estim(s, o) represents the estimated state of the system at time step n if it was estimated in state s at time step n - 1 and if o is observed at time step n.

We impose the estimation strategy to be consistent both across time (i.e. estim is a function) and with the system behaviour (i.e. estim(s, o) belongs to cands(s, o)).

For conciseness purposes, we use "estimation strategy" to refer to "incremental single-state estimation strategy". Given a system and an estimation strategy, the estimation process takes place as follows.

Definition 4 (Estimated sequence). Let M be a system, seqobs be an observation sequence in Lobs (M) and estim an estimation strategy for M. The estimated sequence for seqobs is the state sequence ̂ seq ∈ L(M) such that ̂ seq[0] = s0 and for all i in [1, |̂ seq|-1], ̂ seq [i] = estim( ̂ seq [i -1], seq obs [i]).

Example 1. Let M = (S, s0, O, ∆, obs) be the system represented in Fig. 1. We have S = {s0, . . . , s5}, O = {a, b}, ∆ is represented by the arrows in the figure, obs(s0) = obs(s3) = obs(s5) = a and obs(s1) = obs(s2) = obs(s4) = b.

In this system only two pairs in S × O have more than one estimation candidate: (s0, b) and (s1, a). Let estim1 be the estimation strategy such that estim1(s0, b) = s1 and estim1(s1, a) = s3, and the unique candidate is selected otherwise (for example, cands(s3, a) = {s3} so necessarily estim1(s3, a) = s3).

When the system produces the observation sequence (a, b, a, a), it can be explained by three state sequences in the system: (s0, s1, s3, s3), (s0, s1, s5, s5) and (s0, s2, s5, s5). With the strategy estim1, we select the first one. The estimation process is illustrated in Figure 2 using this strategy.

In Example 1, one can observe that the state s2 cannot be part of any estimated sequence, as the estimation strategy chooses a branch of the system states that does not contain s2. The set of states that the estimation strategy actually uses is denoted ̂ S and is formally defined by the set of states in S that are part of an estimation sequence associated with a sequence of observation in Lobs .

An estimation strategy estim for a system M = (S, s0,O,∆, obs) can also be represented by an estimator, i.e. a 5-tuple ̂ M = (̂ S, s0, O, ̂∆, obs) composed of the reachable states and transitions in the system with the strategy.

Definition 5 (Estimator). Let M = (S, s0,O,∆, obs) be a system and estim an estimation strategy. The estimator induced by estim is a deterministic Moore machine ̂ M = ( ̂ S, s0, O, ̂∆, obs) such that:

• ̂ S ⊆ S is the set of states that belong to some estimated sequence for the given estimation strategy;
• ̂∆ is the smallest subset of ∆ such that ∀̂ s ∈ ̂ S, ∀o ∈ nextObs (̂ s), (̂ s, estim(̂ s, o)) belongs to ̂∆.

In Figure 1, ̂ M1 is the estimator associated with the estimation strategy estim1 introduced in Example 1.

Definition 5 indicates how for a given system, every estimation strategy can be represented by an estimator. Note that the reverse also holds: for a given system M = (S, s0,O,∆, obs), any deterministic Moore machine ̂ M = ( ̂ S, s0,O, ̂∆, obs) such that ̂ S ⊆ S and ̂∆ ⊆ ∆, is in fact an estimator that implements an estimation strategy estim such that estim(ˆ s, o) is the unique ˆ t such that (ˆ s, ˆ t) ∈ ̂∆ and obs(ˆ t) = o, for ˆ s ∈ ̂ S and o ∈ O. In the rest of the paper, we use estimators to represent estimation strategies.

4 Single-State Trackability

4.1 Dead-ends

In this section, we first recall the notion of dead-end as defined in [Bouziat et al., 2019]. During estimation, the estimator may choose a state sequence different from the one taken by the system. This can be particularly problematic when the following conditions happen: a) the system is in state s, the estimator estimates that it is in state ̂ s with ̂ s ̸= s; b) the system moves in state t and produces observation o; c) there exists no candidate ̂t in ̂ S such that obs(̂t) = o and (̂ s, ̂t) belongs to ̂∆.

Definition 6 (Dead-end). A dead-end for an estimator ̂ M of a system M is an observation sequence that belongs to Lobs(M) but does not belong to Lobs(̂ M).

An estimator ̂ M is dead-end free if there is no dead-end for it, i.e. Lobs(M) = Lobs(̂ M).

Example 2. We consider the example illustrated in Figure 1. Let ̂ M2 be the estimator induced by the estimation strategy estim2 defined by estim2(s0, b) = s2 (no other choices necessary). The sequence of observations (a, b, b, b) belongs to Lobs(M) as it is produced by the state sequence (s0, s1, s4, s4) but it does not belong to Lobs(̂ M2). This observation sequence is therefore a dead-end for ̂ M2. Note that ̂ M1 is dead-end free.

In [Kurien and Nayak, 2000], dead-ends are handled by backtracking in time in order to modify previous estimation choices. The main drawback of this technique is the lack of control over both the computational time and memory. Moreover, some actions may have been taken based on the previous estimated states that cannot be undone. Backtracking in time and revising estimations may turn past actions sub-optimal or even inconsistent.

Another way to tackle dead-ends is to keep a fixed number k of past observations and reason on this window [Su et al., 2014]. However this approach is also subject to dead-ends as the estimator and system paths may diverge earlier beyond the memorized window.

Our goal is to design estimators able to follow the execution of a system while keeping just a unique state in memory and never encountering dead-ends. Such deterministic incremental estimators may be feasible depending on the system specifications. We express that possibility by defining singlestate trackability for discrete event systems.

4.2 Trackability Problem

In [Bouziat et al., 2019], a system is considered as singlestate trackable if there exists a dead-end free single-state incremental estimator for this system. They show that this is the case if and only if there exists an estimator with an observation language equal to that of the system. In this paper, we take the language equivalence as a definition of Single-State Trackability.

Definition 7 (Single-State Trackability). A system M is single-state trackable if there exists an estimator ̂ M for M such that Lobs (M) = Lobs (̂ M).

Determining whether a system is single-state trackable or not is called the TRACKABILITY problem.

The problem of deciding if two languages are equivalent (also called trace-equivalence) is, in the general case, a PSPACE-complete problem [H¨uttel and Shukla, 1996]. This leads to the definition of a rather complex algorithm for the TRACKABILITY problem in [Bouziat et al., 2019]. This approach can be improved because the system and the estimator, for which language equivalence is considered, are not independent from each other. In fact, the estimator is a submachine of the system's machine. A contribution of this paper is to prove that in this case, the language equivalence problem is reduced to the simulation preorder problem, which is decidable in polynomial time [Shukla et al., 1996].

We first adapt the definition of simulation to the case of a system and an estimator.

Definition 8 (Simulation for estimators). Let M = (S, s0,O,∆, obs) be a system and ̂ M = (̂ S, s0, O, ̂∆, obs) be an estimator for M. ̂ M simulates M if there exists a relation R ⊆ S × ̂ S such that:

Informally, if s is a state in S and ̂ s a state in ̂ S, then ̂ s simulates s (or (s, ̂ s) is in R) represents the fact that ̂ M can estimate that the system is in state ̂ s while it really is in state s without encountering a dead-end later in the execution.

Proposition 1. Let M be a system and ̂ M be an estimator for M. ̂ M is dead-end free (or Lobs(M) = Lobs(̂ M)) if and only if ̂ M simulates M.

Proof. (⇐) Lobs(̂ M) ⊆ Lobs(M) as the states and transitions of ̂ M are subsets of those of the system. Moreover, let seqobs ∈ Lobs(M) be produced by seq ∈ L(M). We prove that for all k < |seq|, there exists a sequence ̂ seq ∈ L(̂ M) of length k such that obs(seq) = obs(̂ seq) and (seq[k], ̂ seq [k]) ∈ R, which entails Lobs (̂ M) ⊇ Lobs (M). (⇒) We consider the following relation R: ∀s ∈ S, ̂ s ∈ ̂ S, (s, ̂ s) ∈ R iff ∃seqobs ∈ Lobs(M), seq ∈ L(M), ̂ seq ∈ L(̂ M) s.t. obs(seq) = obs(̂ seq) = seqobs , s = last(seq) and ̂ s = last(̂ seq). We show that R is a simulation relation. (1,2) By construction of R, we have (s0, s0) ∈ R, and for all (s, ̂ s) ∈ R, obs(s) = obs(̂ s). (3) Let (s, ̂ s) ∈ R and t ∈ S such that (s, t) ∈ ∆. By construction of R, ∃seqobs ∈ Lobs(M), seq ∈ L(M), ̂ seq ∈ L(̂ M) s.t.

obs(seq) = obs(̂ seq), s = last(seq) and ̂ s = last(̂ seq ). (s, t) ∈ ∆ so seq.t ∈ L(M) and produces the sequence of observation seqobs.obs(t) ∈ Lobs(M). By the equality of languages and definition of Lobs(̂ M), there exists ̂ seq ′ ∈ L(̂ M) s.t. obs(̂ seq ′ ) = seqobs.obs(t). As ̂ M is deterministic, seqobs is generated by the same state sequence ̂ seq. So, ̂ seq ′ is equal to ̂ seq.̂t and (̂ s, ̂t) ∈ ̂∆. By construction of R, (t, ̂t) ∈ R.

The following corollary presents a necessary condition for estimators. It indicates that any observation sequence that can follow a state s can also follow the state ̂ s by which s is estimated. This corollary is used in Section 6 to increase the efficiency of estimator synthesis.

Corollary 1. Let M be a system, ̂ M a dead-end free estimator for M, s a state in S, ̂ s a state in ̂ S, and R a simulation relation such that (s, ̂ s) ∈ R. For any observation sequence seqobs , if seqobs can follow s then seqobs can follow ̂ s.

Corollary 2. The TRACKABILITY problem is in NP.

Proof. Checking if ̂ M is a dead-end free estimator for M is polynomial since it comes to checking whether ̂ M simulates M, which can be encoded into HORN-SAT clauses as shown in [Shukla et al., 1996].

5 Estimator Correctness

Correctness is the property of an estimator that estimates the actual system state. So far we provided a way to generate dead-end free estimators, which can be seen as a very weak form of correctness as a dead-end free estimator cannot be proven wrong by the system's observations. However, depending on the operational context, total correctness may be required or an incorrect pessimistic or optimistic estimation may be satisfying [Bouziat et al., 2018; Couto et al., 2020].

In this section, we model correctness as constraints and optimization criteria that allow some end-user to generate interesting estimators. Correctness constraints allow one to restrict the possible estimator states associated with some given system state. Correctness criteria let one associate a cost with each possible estimator, with the lowest cost being associated with the "most correct" estimators.

Definition 9 ((φ1, φ2)-correctness). Let M be a system, φ1 ⊆ S and φ2 ⊆ S be two sets of states of M, ̂ M a dead-end free estimator for M, and R the associated simulation relation. ̂ M is (φ1, φ2)-correct if whenever the system is in a state of φ1, then the estimator is in a state of φ2, i.e. ∀(s, ̂ s) ∈ R, if s ∈ φ1 then ̂ s ∈ φ2.

In a symbolic model where states are represented by Boolean variables, correctness constraints can be represented by propositional formulae. They can also be deduced from a proof of reachability of an undesirable pair (s, ˆ s) as produced in [Couto et al., 2020]. With such constraints, one can require that whenever some critical fault is present in the system state, it is also present in the estimated state. This ensures the estimator is correct with respect to this critical fault.

Example 3. Let us consider the system M presented in Example 1 and illustrated on Figure 1. Let f1 be a fault only present in states φf1 = {s1, s3, s4} and f2 a fault only present in φf2 = {s5}. The estimator ̂ M1 is (φf1 , φf1 )- correct as all the states in φf1 are estimated by states in φf1 . However ̂ M1 is not (φf2 , φf2 )-correct as s5 is estimated by s3 which does not belong to φf2 .

While it is very flexible, in some systems, (φ1, φ2)- correctness might be either too strong or too tedious to specify. For example, in Example 3, there exists no estimator that satisfies both (φf1 , φf1 ) and (φf2 , φf2 )-correctness. In order to relax this requirement, a first laborious approach is to enumerate the possible estimated states for each system state. Another approach consists in expressing a weaker form of correctness, for instance that (φ1, φ2)-correctness should be satisfied "as much as possible". In this regard we introduce a cost function that lets one model this kind of requirement.

Definition 10 (Correctness cost). Let M be a system, ̂ M an estimator for M, and R their simulation relation. Let cost : S× ̂ S → N be a cost function such that cost(s, ̂ s) represents how much we want to avoid estimating that the system is in state ̂ s when its real state is s. The correctness cost for ̂ M is cost(̂ M) = ∑(s,̂ s)∈R cost(s, ̂ s)

Definition 11 (Correctness order). Let M be a system, ̂ M1 and ̂ M2 be two dead-end free estimators for this system, and cost a cost function. ̂ M1 is strictly more correct than ̂ M2 with respect to cost if cost(̂ M1) < cost( ̂ M2).

There are several ways to define a cost for pairs of states. A straightforward one is to check if the real state of the system is correctly estimated. Such a cost c= is formally defined by ∀(s, ̂ s) ∈ S2 , c=(s, ̂ s) = 0 if s = ̂ s, 1 otherwise. One could also consider a cost based on (φ1, φ2)-correctness: ∀(s, ̂ s) ∈ S2 , cφ1,φ2 (s, ̂ s) = 0 if s ∈ φ1 and ̂ s ∈ φ2, 1 otherwise. Symbolic models make it easier to specify cost functions. The Hamming distance ([Hamming, 1950]) is an example of a cost function for Boolean variables. Weighted sums, or lexicographical aggregation of costs can also be used to emphasize some critical faults for example.

Example 4. Let us consider the system M presented in Example 1 and illustrated on Figure 1. We define the dead-end free estimator ̂ M3 similar to ̂ M1 except that estim3(s1, a) = s5. We consider a correctness cost c such that ∀i, c(si, si) = 0, c(s1, s2) = c(s2, s1) = 1, c(s5, s3) = 1 and c(s3, s5) = 2. This cost represents that it is preferable to estimate that the system is in state s3 when it really is in state s5 than the opposite. We have c( ̂ M1) = 2 and c( ̂ M3) = 3. This means that ̂ M1 is more correct than ̂ M3 with respect to cost c.

6 Estimator Synthesis

In this section, we describe a procedure to solve the TRACKABILITY problem. To decide if a system M is single-state trackable, we try to synthesize a dead-end free estimator for it. More precisely, we consider that a systemM can be seen as a graph and that a dead-end free estimator ̂ M is a sub-graph that satisfies several constraints, that can be encoded into SMT provided the underlying theory provides graph predicates. We specifically target the solver MONOSAT ([Bayless et al., 2015]), that allows to handle classical SAT constraints but also graph constraints.

Dead-end free estimator synthesis. Let M = (S, s0,O,∆, obs) be a system and ̂ M = (̂ S, s0, O, ̂∆, obs) the dead-end free estimator we try to synthesize for M. If ̂ M exists (i.e. M is single-state trackable), then states and transitions of ̂ M are subsets of those of M and following Prop. 1, there exists a simulation relation R between the states of M and ̂ M.

We associate the system M with a directed graph G whose vertices are the states S and whose edges are the transitions ∆. Similarly, ̂G is the graph associated with an estimator ̂ M. First, we instantiate the following Boolean decision variables:

• for each s ∈ S, vs is true iff s belongs to ̂ S;
• for each (s, t) ∈ ∆, es,t is true iff (s, t) belongs to ̂∆;
• for each (s, ̂ s) in S2 , rs,̂ s is true iff (s, ̂ s) belongs to R. We next instantiate the following constraints.

We first encode that the estimator is a well-built automaton. Constraint (4) states that if an edge is selected in ̂G, its vertices are selected as well. Constraint (5) enforces the states of the estimator to be exactly the ones reachable from s0 in the graph ̂G. We use here the MONOSAT predicate reachable.

Constraints (6) and (7) force ̂ M to be deterministic: for every state s and every successor observation o, exactly one outgoing transition leads to a state with observation o. We use two constraints, as in SAT/SMT the "at most one" cardinality constraint (6) cannot easily be combined with the implication of Constraint (7).

We next consider constraints related to the simulation relation. Constraint (8) states that the initial state simulates itself (see Definition 8). Constraint (9) encodes that every state of the system is simulated by at least one state of the estimator. Constraint (10) encodes the simulation relation from Definition 8 and also states that the edge associated with the simulation relation must belong to ̂ M 1 .

Constraint (11) makes the simulation relation minimal as the estimator states must all simulate at least one system state.

Using a SMT solver let us use the predicate reachable in constraint (5). This constraint can be expressed in SAT clauses using for instance the Floyd-Warshall algorithm [Cormen et al., 2001] with a complexity of O(|V |3 ). MONOSAT achieves a complexity of O(|V | · |E|) [Bayless et al., 2015].

From Definition 8 and Corollary 1, the number of variables rs,̂ s can be reduced by creating variables only for pairs (s, ̂ s) for which ̂ s accepts all the observation sequences of length 2 (or more) that s accepts.

Correct estimator synthesis. The encoding presented above allows to synthesize dead-end free estimators. It is possible to enrich it to synthesize correct estimators, as defined in Section 5. (φ1, φ2)-correctness can be encoded as a hard constraint the following way: ∀s ∈ φ1, ∀̂ s ∈ S \ φ2, ¬rs,̂ s. The second correctness requires a cost function c as input, and is encoded as the following pseudo Boolean criterion: minimize ∑(s,̂ s)∈R rs,̂ s · c(s, ̂ s).

7 Experiments

Our implementation uses the SCALA programming language, and each experiment was performed on a computer with a Intel R© Xeon R© CPU E5-2699 v3 @ 2.30GHz processor and a limit of 16GB of memory.

Examples from the literature. We have encoded benchmarks from three system models from the literature:

• valve controller [Sampath et al., 1995] that models a valve controller for heating, ventilation and air conditioning units with a valve that can be stuck closed or stuck open, a pump that can fail in modes on and off and a controller; each component has 4 possible states; this system is not trackable.
• valve driver [Williams and Nayak, 1996] that models a valve driver that has 4 modes, 6 command inputs and 3 command outputs; this system is trackable.
• baggage transfer [Pencol´e et al., 2018] that models a baggage transfer system composed of 2 conveyors, 1 piston, 1 controller and 4 sensors. No fault model is provided, so we enriched each component with a permanent fault model. By enabling or not the fault model for each of the 8 components, we managed to create 218 systems among 256, all of which are trackable.

Random examples. In order to test our prototype intensively, we randomly generated a set of systems as follows. First, we generated a set of small systems of 5 states, 3 observations, and 0.5 transition probability for any two states. Second, we aggregated them by Cartesian product (of states and observations), with a 0.1 probability that any two states are incompatible (in this case their pair is removed from the aggregated states). The benchmark contains systems obtained by aggregation of 4 and 5 small systems. Finally, we selected only "interesting" systems, such that:

1 Note that Constraint (9) is redundant with Constraints (8) and (10), but improves the solver's performance.

1. the system is trackable;
2. the estimator has less than half the number of states of the system (so as to reject trivially trackable systems);
3. there exists a state s such that the systemhas no ({s}, S\ {s})-correct estimator.

This method generated systems from 10 to 1461 states, with more small systems than large ones.

Analysis. In all our experiments, most of the computation time is used for generating SMT clauses whereas the time required by MONOSAT to solve the SMT instance is negligible. This explains why the computation time is nearly the same for the trackable and untrackable versions of random examples. We have yet to properly assess the impact of a cost function on the solving time. Figure 3 shows that on random benchmarks, the solving time grows regularly in the number of states. The valve driver and valve controller systems require similar computation time as random systems. For the baggage transfer system, the computation time is higher, because of the large number of symmetries in the system.

8 Conclusion

This paper describes a new approach for checking single-state trackability as defined in [Bouziat et al., 2019]. As a system is simulated by its estimator, we prove that the TRACKABILITY problem is in NP. We also define two customizable correctness types for modelling relevant estimators. We solve the TRACKABILITY problem by reducing it to a MONOSAT SMT query, along with correctness requirements. The approach is validated on a set of benchmarks both from the literature and from randomly generated problems.

Studying NP-completeness with and without correctness constraints is a natural next step in our work. Allowing for delayed estimation, or using a bounded number of memorized states at each time step could help apply this approach to a larger range of systems, including real-world systems, and will be considered in future work.

Symbolic representation of estimators with preferences as in [Bouziat et al., 2018] is also a possible extension.