ABSTRACTION DES TRAJECTOIRES D’UN SYSTEME CONTINU EN AUTOMATES TEMPORISES

30/09/2017
Publication e-STA e-STA 2004-3
OAI : oai:www.see.asso.fr:545:2004-3:20050
DOI :

Résumé

ABSTRACTION DES TRAJECTOIRES D’UN SYSTEME CONTINU EN AUTOMATES  TEMPORISES

Métriques

23
6
326.65 Ko
 application/pdf
bitcache://dce4dbae1c8a2d53a6eeb581a7d3c110a20c2cb5

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/545:2004-3/20050</identifier><creators><creator><creatorName>Arnaud Hélias</creatorName></creator><creator><creatorName>François Guerrin</creatorName></creator><creator><creatorName>Jean-Philippe Steyer</creatorName></creator></creators><titles>
            <title>ABSTRACTION DES TRAJECTOIRES D’UN SYSTEME CONTINU EN AUTOMATES  TEMPORISES</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2017</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Sat 30 Sep 2017</date>
	    <date dateType="Updated">Sat 30 Sep 2017</date>
            <date dateType="Submitted">Fri 10 Aug 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">dce4dbae1c8a2d53a6eeb581a7d3c110a20c2cb5</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>34067</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

ABSTRACTION DES TRAJECTOIRES D’UN SYSTEME CONTINU EN AUTOMATES TEMPORISES ABSTRACTION OF CONTINUOUS SYSTEM TRAJECTORIES INTO TIMED AUTOMATA Arnaud HÉLIAS1,2,* , François GUERRIN1 and Jean-Philippe STEYER2 1 CIRAD, Gdor team, Station de la Bretagne, BP 20, 97408 Saint-Denis, Reunion Island, France, guerrin@cirad.fr 2 INRA, Laboratory of environmental biotechnology, av. des étangs, 11100 Narbonne, France, steyer@ensam.inra.fr Résumé: Cet article traite de la représentation de la dynamique d’un système continu par un formalisme à événements discrets et temps continu, à des fins d’analyse de système. Le système continu est d’abord approximé à l’aide d’intervalles numériques, puis traduit dans le formalisme des automates temporisés grâce à l’introduction de seuils partitionnant les domaines de valeurs des variables d’état. La détection des franchissements de seuil est caractérisée par deux instants correspondant à la date au plus tôt et à la date au plus tard de franchissement. Cette approche est brièvement illustrée sur un procédé pilote de traitement d’eaux usées de 1 m3 . Mots clés: Approximation de modèle, Système discret, Système continu, Intervalles, Seuils, Automates, Traitement des déchets. Abstract: This paper deals with the representation of continuous system dynamics into a continuous-time discrete-event formalism to the end of system analysis. The continuous system is first approximated by using numerical intervals and then translated into the timed automata formalism thanks to with the introduction of thresholds partitioning the state variables’ domains. The detection of thresholds crossing is characterised by two time instants corresponding respectively to the earliest and latest crossing dates. This approach is briefly illustrated on a 1 m3 wastewater treatment pilot plant. Keywords: Model approximation, Discrete system, Continuous system, Intervals, Thresholds, Automata, Waste treatment. * Current author’s address: INRA, Food Process Engineering and Microbiology Laboratory, BP 01, 78850 Thiverval-Grignon, France, arnaud.helias@grignon.inra.fr. 1. INTRODUCTION A classical approach to analyse the interaction between continuous and discrete elements within a system is to represent it with a unique formalism. In the Qualitative reasoning and Hybrid dynamical system communities, this problem was often addressed. However, Struss (2002) underlined three main difficulties: (i) explosion in the number of discrete states , (ii) rounding errors of intermediate variables and (iii) thresholds detection. Moreover, time is not often clearly represented. This study is based on a timed discrete-event representation similar to those developed by Henzinger et al. (1998), Kowalewski et al. (1999), Lunze (1999), Supavatanakul et al. (2003); however it differs from several points: −as the continuous system dynamics is assumed to be partially known, the resulting imprecision is represented by numerical intervals bounding both initial states and input variables values; −thresholds, partitioning the state-variable domains according to expert knowledge are used as a basis of the state space discretisation; −to avoid combinatorial explosion, timed automata are purposely built to answer specific questions, according to some initial state and the properties to be checked. The paper is organised as follows. After a brief recall on timed automata, one of the most widespread timed discrete formalism, the continuous system under study is described in Section 2. The discretisation procedure is then detailed in Section 3 and illustrated by an application example in Section 4. Finally, this approach is briefly discussed in Section 5 and conclusions are drawn in Section 6. 2. SYSTEM FORMAL DESCRIPTION Timed automata Introduced by Alur and Dill (1994), a timed automaton is composed by a finite state machine and the expression of continuous time. This formalism allows timed constraints to be introduced using variables named clocks. Clock. , with X a finite set, is a clock whose value grows linearly with time (i.e., ∈ x X ( ) ( ) t t ε ε + = + x x with ε a positive time lapse and x’s derivative always equal to 1). Clock constraint. A clock constraint is an atomic constraint conjunction. Taking x and y two clocks, a constant and # a symbol relation from the set , the set of the atomic constraints c ∈ { , , , , < ≤ = ≥ >} ( ) Φ X ϕ is defined by the grammar 1 # | # | c c 2 ϕ ϕ ϕ := − ∧ x x y . These constraints are possibly associated to the locations or edges of the automaton. Timed automaton. A timed automaton G is defined by a 6-tuple ( ) with: , , , , , S P X E A Inv −S a finite set of locations with the initial location; 0∈ s S − P a mapping which associates to each ∈ s S , a set of atomic propositions valid at this location; −X a finite set of clocks; −E a finite set of labels; − a finite set of edges; each edge a is a 5-tuple ( ) 2 Φ ⊆ × × × × X A S E X S ( ) , , , , ϕ δ ′ s e s with ∈ s S the start location and the destination location, a clock constraint named guard that must be satisfied to trigger the discrete transition and ′∈ s S ( ) ϕ Φ ∈ X δ ⊆ X the clock subset to be reinitialised during the transition; − a mapping that associates to each location a timed constraint ( ) ( ) Φ : → Inv s S X ϕ′, named invariant. The system can remain in the same location as long as the invariant is true. Continuous system We consider a non-linear piecewise continuous system described by an ordinary differential equation (ODE) system such as: 0 0 ( , ) ( ) f t ξ ξ ζ ξ ξ ⎧ = ⎪ ⎨ = ⎪ ⎩ (1) where , with Ξ a n-dimensional state space, n ξ Ξ ∈ ⊆ ( , ) g p t ζ = , , with Ζ a m- dimensional input space, and a parameter. It is assumed that we have only a partial knowledge of both the initial state m ζ Ζ ∈ ⊆ p P ∈ ( ) 0 t ξ and the input variables values ζ that can be estimated by: (2) 0 0 0 i i i , ( ) ( ) ( ) i t t t ξ ξ ξ − + ∀ ≤ ≤ ( ) ( ) ( ) , , j j j j t t t t ζ ζ ζ − + ∀ ∀ ≤ ≤ (3) with {1,..., } i n ∈ , {1,..., } j m ∈ , 2 ( , ) i i i ξ ξ Ξ − + ∈ and 2 ( , ) j j j ζ ζ Ζ − + ∈ ( i Ξ Ξ ⊂ and ). j Ζ Ζ ⊂ Uncertainty representation. We define ζ < and ζ > according to the influence of the interval bounds on the derivative’s values (taking ): {1,..., }\{ } k m = j j j ( , , ) ( , ) ( , , ) , ( , , ) ( , ) ( , , ) , i k j i i k j j j j i k j i i k j j j j f f f f f f ξ ζ ζ ξ ζ ξ ζ ζ ζ ζ ζ ζ ξ ζ ζ ξ ζ ξ ζ ζ ζ ζ ζ ζ − + < − > + − + < + > ≤ ≤ ⇒ = = ≥ ≥ ⇒ = = − (4) From (4) we can rewrite (1) as the double ODE system: 0 0 0 0 ( , ) ( ) ( , ) ( ) f t f t ξ ξ ζ ξ ξ ξ ξ ζ ξ ξ − − < − − + + > + + ⎧ = ⎪ = ⎪ ⎪ ⎨ ⎪ = ⎪ ⎪ = ⎩ (5) With the property , Eq. (5) can approximate the system (1) by introducing uncertainty on the initial state (Eq. (2)) and the system inputs (Eq. (3)) if the cooperativity property is verified on the system’s dynamics (Smith 1995). Cooperativity simply states that the off-diagonal elements of the Jacobian matrix of a dynamic system are positive or equal to zero (additional details can be found in Gouzé et al., (2000) or Moor and Raisch (2002)). , , ( ) ( ) ( ) i i i t i t t t ξ ξ ξ − + ∀ ∀ ≤ ≤ Threshold To represent the continuous system dynamics in a discrete formalism, the first step is to discretise the state space. For this, each i ξ ’s domain is partitioned according to thresholds into a finite number of intervals that can be considered as qualitative states. Thresholds are defined from expert knowledge; e.g., a stock level can be qualified as “insufficient”, “low”, “medium”, “high” and “critical”. denotes the ordered set of thresholds in the ith dimension, that is, with i L { } 1 i ,...,n ∈ and : i Ω ∈ (7) ( ) { ,0 , , ,..., i i i i L l l Ω < = } } The continuous state space Ξ is divided according to the thresholds by the mapping: i i Ω ∏ { } { 1 : 1,..., ... 1,..., X i D Ξ Ω → × × Ω (8) with the assumption that . A rectangular partition is thus obtained. ,0 , , , i i i i l l i Ω ξ ⎡ ⎤ ∈ ∀ ⎣ ⎦ 3. DISCRETE APPROXIMATION The idea is (i) not to consider as discrete states the cells partitioning the state space themselves but, rather, the cells’ faces and (ii) determine the state transitions from the simulation output of the continuous system within each cell as was done by Kowalewski et al., 1999. These authors defined a grid on each cell’s face and simulated all the trajectories from or bounded to each grid-point. In comparison, our approach depends upon each considered initial state and focuses on handling uncertainty by propagating the interval , ξ ξ − + ⎡ ⎤ ⎣ ⎦ within the cells by simulating Eq. (5). Trajectories within a cell Thresholds crossing. Let τ be the time-point when the system (1) reaches v, a threshold value defined in the ith dimension, i.e., ( ) , i v v ξ τ = ∈ . Because ξi is estimated by the interval , i i ξ ξ − + ⎡ ⎤ ⎣ ⎦ , the time window within which crossing the v threshold may occur can be described by τ − and τ + such that . From Eq. (5), the following implications can then be set: ( ) ( ) i i v ξ τ ξ τ − − + + = = ( ) ( ) ( ) ( ) 0 0 i i ξ τ ξ τ τ − − + + + − > ∧ > ⇒ <τ (9) ( ) ( ) ( ) ( ) 0 0 i i ξ τ ξ τ τ − − + + + − < ∧ < ⇒ >τ (10) Timed automaton representation. Let min( , ) min τ τ τ − + = , max( , ) max τ τ τ − + = and F the mapping that associates a label to each threshold crossing: ( ) " " if " " if min min v τ τ τ τ ∆ + ∇ − ⎧ = ⎪ → ⎨ = ⎪ ⎩ v v F (12) with the symbols ∆ and ∇ denoting threshold crossing with increasing and decreasing trends respectively. min τ and max τ being approximated on (cf. the clock constraint definition), the system trajectory between two thresholds w and v is represented within the time window [ ] , min max τ τ . This window can be modelled in the timed automata formalism as follows (cf. Fig. 1): −s1 and s2 are two locations with associated labels and " " " ∆ w " ∆ v respectively, −x is a clock, − max τ ≤ x is the invariant of s1, − ( ) 1 2 , , , , min τ ∅ ≥ ∅ s x s is the edge. max τ ≤ x min τ ≥ x "w∆" "v∆" s1 s2 t v i ξ− i ξ+ τ− τ+ Ξi w Fig. 1. Timed automaton for describing a system’s trajectory from thresholds w to v with an increasing trend. Generalisation For sake of clarity, the index i is omitted in notations for all the variables in the following sections. Applying the above described approach to the lower bound of Eq. (5) in the ith dimension allows one to obtain Τ − , the ordered set of time instants when ξ− crosses the thresholds and , the ordered set of threshold crossings: Σ − ( ) { } , ( ) j j lω Τ τ ξ τ − − − − ≤ = = (13) ( ) { } , j j j ( ) Σ σ σ ξ τ − − − − ≤ = = − (14) with 1,..., j J = , and ( ) ( ) card card J T Σ − − = = { } 1,..., ω Ω ∈ . In the following, the mapping that associates min τ or max τ to each j τ − according to the sign of the derivative is denoted : Τ − A (15) ( ) ( ) if 0 : if 0 min j j max j Τ τ ξ τ τ τ ξ τ − − − − − − ⎧ < ⎪ ⎨ > ⎪ ⎩ A A similar approach can be used on the upper bound to obtain Τ + , Σ + and associated labels by the mapping Τ + A . Building the timed automaton associated to the system’s trajectory in the ith dimension From Eqs. (13-15), the following sets can be defined: −B, the ordered set of time instants when occur threshold crossings by ξ− and ξ+ with label min τ ( 1,..., B B k K = , ( ) ( ) card card B K B D = = ): ( ) { } { } , ( ) ( ) B B B B k k k k B b b b b Τ Τ Τ τ Τ τ − + − + ≤ = ∈ = ∈ = ∪ A A min min (16) −C, the ordered set of time instants when occur threshold crossings by ξ− and ξ+ with label max τ ( , 1,..., C C k K = ( ) card C K C = ): ( ) { } { , ( ) ( ) C C C C k k k k C c c c c Τ Τ Τ τ Τ τ − + − + ≤ = ∈ = ∈ = ∪ A A } max max (17) −D, the ordered set of threshold crossings associated to the elements of B: ( ) { } { , ( ) ( ) B B B B k k k k D d b d d b Σ ξ Σ ξ − − + + ≤ = ∈ = ∈ = ∪ } B B k k d ) ) (18) − , the set of threshold crossings with decreasing trends at the initial time ( , ): 0 Σ ∇ 1,..., k K Σ Σ ∇ ∇ = ( card KΣ Σ ∇ ∇ 0 = (19) ( ) ( ) { } ( ) ( ) ( { } ( ) ( ) ( ) { } 0 0, 0, 0, 0, 0, 0, 0, 0, 0, | | 0 | 0 k k k k k k k k k L L L Σ Σ Σ Σ Σ Σ Σ Σ Σ Σ σ σ ξ σ ξ σ σ ξ σ ξ σ σ ξ σ ξ ∇ ∇ ∇ ∇ ∇ ∇ ∇ ∇ ∇ ∇ ∇ ∇ − ∇ + ∇ ∇ − ∇ − ∇ ∇ + ∇ + = ∈ ∧ < < ∈ ∧ = ∧ ≤ ∈ ∧ = ∧ ≥ ∪ ∪ − the set of threshold crossings with an increasing trend at the initial time ( , ): 0 Σ ∆ 1,..., k K Σ Σ ∆ ∆ = ( ) card KΣ Σ ∆ ∆ 0 = ( ) ( ) { } ( ) ( ) ( ) { } ( ) ( ) ( ) { } 4 4 0 0, 0, 0, 0, 0, 0, 0, 0, 0, | | 0 | k k k k k k k k k L L L Σ Σ Σ Σ Σ Σ Σ Σ σ σ ξ σ ξ σ σ ξ σ ξ σ σ ξ σ ξ ∆ ∆ ∆ ∆ ∆ ∆ ∆ ∆ ∆ ∆ − ∆ + ∆ ∆ − ∆ − ∆ ∆ + ∆ + = ∈ ∧ < < ∈ ∧ = ∧ ≥ ∈ ∧ = ∧ ≤ ∪ ∪ 0 ∪ (20) Clock set. The clock set is a singleton since the automaton is obtained from only one simulation of the continuous model. Location set. Let us denote: − S , a mapping that associates a location s to each element of D, and . From S , one gets with 0 Σ ∇ 0 Σ ∆ { } 0 1,..., k k K = = S s s B K K K K Σ Σ ∇ ∆ + = + and s0, the location corresponding to the initial state of the continuous system. −P, a mapping that associates a proposition to each element of S denoting which threshold is crossed and the trend (with ω Ω ∈ and with ): ( ) 0 0 → P s l ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) ( ) 0, 0, 0, 0, : B B B B B B k k k k k k k k k k k k k k k d d l d d d l d l l Σ Σ Σ Σ ω ω ω ω ω ω ω ω Σ Σ σ σ σ σ ∇ ∇ ∆ ∇ − ∇ + ∆ ∇ ∇ ∇ ∆ ∆ ∆ ⎧ → ∧ = ∧ = ⇒ ⎪ ⎪ → ∧ = ∧ = ⇒ ⎪ ⎪ →⎨ → ∧ = ⇒ ⎪ ⎪ ⎪ → ∧ = ⇒ ⎪ ⎩ s l s l P s s l s l S S S S (21) Forward edges. Edges that can reach a new location at the earliest time point min τ are named Forward edges. Let , a location corresponding to a threshold crossing with increasing trend, and its associated proposition , n n K ∈ s B ω ∆ l . The preceding location can reflect the following cases (cf. Fig. 2): a)crossing a lower threshold with increasing trend, b)crossing the same threshold with decreasing trend, c)the initial state whenever no threshold has already been crossed and (i) the threshold is within the initial state interval, or (ii) the initial state interval lies below the threshold. The same reasoning can be made the other way around about threshold crossing with a decreasing trend (i.e. about a location with a proposition ω ∇ l ). t w v i ξ − i ξ + 0 t Ξi τmin τmin t v i ξ − i ξ + 0 t Ξi a) b) t v i ξ − i ξ + 0 t Ξi w τmin t v i ξ − i ξ + 0 t Ξi c.i) c.ii) Fig. 2. Different cases of threshold crossing with increasing trend. Based on this, a set of locations can be obtained which satisfy one of these conditions. The preceding location is the element to which is associated the nearest min τ of the min τ of . Formally, a1, the forward edge of is defined by the 5-tuple n s n s ( ) , , , , m n ϕ ∅ ∅ s s with n b ϕ := ≥ x 1 . Let the ordered set , the union of the different cases described by the Fig. 2: ′ ⊂ S S ( ) ( ) ( ) ( ) ( ) { } ( ) ( ) ( ) ( ) { } 1 1 1 , n k k n k k ω ω ω ω ∆ ∆ − ∇ ∇ + ⎧ = ⇒ = ⎪ ′ ≤ = ⎨ ⎪ = ⇒ = ⎩ P s l s P s l S P s l s P s l (23) ( ) ( ) ( ) ( ) ( ) { } ( ) ( ) ( ) ( ) { 2 , n k k n k k ω ω ω ∆ ∇ ∇ ⎧ = ⇒ = ⎪ ′ ≤ = ⎨ ⎪ = ⇒ = ⎩ P s l s P s l S P s l s P s l } ω ∆ (24) ( ) ( ) ( ) ( ) { } 3 4 3 , , n k n k σ σ ∇ ∆ 0 0 ′ = = ∨ = ⇒ S s s s S S 0 (25) ( ) ( ) ( ) ( ) ( ) ( ) ( { } ( ) ( ) ( ) ( ) ( ) ( ) ( { } 1 1 1 0 0 4 0 0 1 n k n n k n d l t t l d l t t l ω ω ω ω ω ω ξ ξ ξ ξ ∆ − + − ∇ − + + ⎧ = ∧ = ∧ ⎪ ⎪ < ≤ ≤ ⇒ ⎪ ′=⎨ = ∧ = ∧ ⎪ ⎪ ⎪ < ≤ ≤ ⇒ ⎩ s P s l s S s P s l s S S ) ) 0 0 4 ′ − (26) (27) ( ) 1 2 3 , ′ ′ ′ ′ ≤ = ∪ ∪ ∪ S S S S S with (i.e., only reachable locations before sn are taken). The preceding location 1,..., 1 k n = m ′ ⊆ s S is the latest that could be reached. The set of locations of forward edges is named S 1 A . A similar approach can be used about the latest time points (i.e., threshold crossing at max τ ) to determine the location’s invariants. Moreover, when a location has no next location, a Backward edge is defined. Figure 3 shows this case: the system crosses a threshold successively twice, and the edge with guard 2 v τ + = x is a backward edge. Doing this, the Inv mapping, that associates the invariants to the locations, and 2 A , the set of backward edges, are defined. A complete description of this approach can be found in Hélias, (2003). t v i ξ − i ξ + 0 t Ξi 1 v τ + 2 v τ + 3 v τ + 1 v τ − "v2 ∆" 1 v τ + x ≥ "0" x ≤ 1 v τ − "v1 ∆" x ≤ 2 v τ + 3 v τ + x ≥ x = 2 v τ + Fig. 3. Backward edge example. From (16-27), the continuous system dynamics in the ith dimension is approximated by the timed automaton where: ( , , , , , i i i i i i i = G S P X E A Inv ) i ∪ − is a set of locations, { } 0, 1,..., i i i i k k K = = S s s −Pi is a mapping that determines, for each location, the threshold crossing and its trend, i 1 If the location is an initial state threshold crossing, then the guard is of the form . 0 t = x −Xi is a singleton composed of the clock xi, −Ei, the set of labels, is an empty set, − 1, 2, i i = ∪ A A A is the set of edges, −Invi is a mapping that associates the invariants to the locations. 4. EXAMPLE: APPROXIMATION OF A WASTEWATER ANAEROBIC DIGESTION MODEL To briefly illustrate this approach, the procedure previously described is used on an anaerobic digestion process. A more complete description of this example can be found in Hélias et al., (2004). The aim is to predict possible dysfunctions of a wastewater treatment plant by a discrete approximation of a biological reaction model in front of expert partial knowledge of the system’s dynamics. Anaerobic digestion is a biological process used for carbon removal from wastewater. The principle is to transform organic matter into biogas (i.e., that is a methane (CH4) and carbon dioxide (CO2) mixture) in absence of oxygen. This complex process can be modelled in two steps: the acidogenic and methanogenic phases. A simplified version of the mass balance analytical model of our process (Bernard et al. , 2001) is used: (28) ( ) ( ) ( ) ( ) 1 1 1 1 1 1 2 2 2 2 1 1 3 2 4 1 1 2 2 in in in in P S D S S k X S D S S k X k X Z D Z Z C D C C k X k X µ µ µ µ µ ⎧ = − − ⎪ = − + − ⎪ ⎨ = − ⎪ ⎪ = − + + ⎩ 2 with 2 2 CO 5 6 T CO P P k k k P P = − − . S1, S2, Z, and C are the organic matter concentration, the volatile fatty acids concentration, the total alkalinity and the total inorganic carbon, respectively. k1 to k6 are the yield coefficients for the reactions and 1 µ and 2 µ are the growth rates of the bacterial biomass X1 according to S1 (in the acidogenic phase) and bacterial biomass X2 according to S2 (in the methanogenic phase) respectively. These growth rates are assumed to follow a Monod-type kinetics, i.e. max S S S K µ µ = + with max µ the maximum bacterial growth rate and S K the half-saturation constant. Finally, is the total pressure in the reactor, is the partial pressure of CO2, D is the dilution rate according to input flow and , , T P 2 CO P 1in S 2in S in Z and the different influent concentrations. Because of a relation holding between and , the cooperativity property holds in this model. Thus, intervals bounding influent and biomass concentrations can be used to handle imprecision, following the approach described in Section 2.. This model is run with parameters measured on an anaerobic digestion pilot plant in C T P 2 CO P (Steyer et al., 2002). The inputs of the process (i.e., influent concentrations) and the initial state are thus represented by intervals. Qualitative states resulting from expert knowledge (e.g., S2 can be assigned labels “normal”, “high” or “critical”) also available are used in this approach. The plant operation is apprehended on a short time period (a few days) by combining information on different variables. For example, an important organic overload (i.e. dysfunction due to an inhibition of the reaction by S2) can be associated to a “low” Z value and a “high” S2 value according to thresholds specifically set in these variables’ domains. To check the possible occurrence of this situation, we use the model-checking tool on the obtained timed automaton. This approach has been used to check about fifteen operating states during a four days period (Hélias et al., 2004). The complete abstraction procedure (system simulation, threshold crossing detection, timed automata creation), with 11 thresholds defined on 4 variable domains, takes less than ten seconds on a personal computer with a CPU running at 1.7 GHz. This procedure has been implemented by combining the Matlab® environment and the Kronos model-checker (Yovine, 1997). The resulting automaton is composed of 24 locations and 66 edges. 5. DISCUSSION The final size of the automaton is set according to the system’s dimension, the number of thresholds and the crossing number. Consequently, this approach is inappropriate when: −the system oscillates around a threshold value, −a large number of thresholds are defined. The idea is not to create an automaton to check all the possible properties of the continuous system but, rather, to create the automaton specifically suited to check a given property according to purposely defined thresholds. Whereas in the classical definition of timed automata the clock constraints compare the clock values using rational numbers, integers must be used in the Kronos model-checker. Consequently, in our approach, the threshold crossing time values must be rounded. Thus, if the time unit used in the model is not carefully chosen according to the system dynamics, some additional imprecision may be introduced. 6. CONCLUSION This paper has described a procedure aimed at representing a continuous system’s dynamics as a timed automaton, where: −some elements (inputs, initial state) are estimated by intervals, which comes down to reformulate the system as extremal ODE systems (upper and lower bounds ξ− and ξ+ approximating the real dynamics), −dynamical envelopes stemming from the simulation of this extremal ODE systems are translated into the timed automata formalism (discrete model with continuous time) according to expert defined thresholds on the state variables’ domain. The principal characteristics of this approach are: −taking threshold crossings themselves as qualitative discrete states (disregarding the interval between two consecutive thresholds); −defining the discrete state transitions from the piecewise simulation of the extremal ODE systems within consecutive thresholds; −starting the procedure from (i) an initial state, (ii) imprecise values of inputs and (iii) threshold definitions, all defined in accordance to the property to be checked in order to reduce the state explosion. This approach was briefly illustrated on an anaerobic digestion model. The timed discrete-event representation makes model-checking possible to check properties of the continuous system’s dynamics. An interesting extension would be to couple this representation to the discrete part of a wastewater treatment process in order to check properties on mixed continuous and discrete elements. ACKNOWLEDGEMENTS This work was partially supported by the Région Réunion and the European Social Fund. A first version of this paper was published at IFAC Workshop on Discrete Event Systems, WODES'04, 22-24 September 2004. REFERENCES R. Alur and Dill D. (1994). The theory of timed automata. Theor. Comp. Sc.. 126: pp. 183-235. O. Bernard, Hadj-Sadok Z., Dochain D., Genovesi A. and Steyer J.-P. (2001). Dynamical model development and parameter identification for anaerobic wastewater treatment process. Biotech. and Bioengineering. 75(4): pp. 424-438. J.L. Gouzé, Rapaport A. and Hadj-Sadok M.Z. (2000). Interval observers for uncertain biological systems. Ecological Modelling. 133(1-2): pp. 45-56. A. Hélias (2003). Agrégation/abstraction de modèles pour l'analyse et l'organisation de réseaux de flux : application à la gestion des effluents d'élevage à la Réunion. PhD thesis. ENSAM. Montpellier (France). 224 p. A. Hélias, Guerrin F. and Steyer J.-P. (2004). Abstracting continuous system behaviours into timed automata: application to diagnosis of an anaerobic digestion process. In Proc. DX-2004 15th International Workshop on Principles of Diagnosis. Carcassonne (France). T.A. Henzinger, Ho P.-H. and Wong-Toi H. (1998). Algorithmic Analysis of Nonlinear Hybrid Systems. IEEE Trans. on Automatic Control. 43(4): pp. 540-554. S. Kowalewski, Engell S., Prußig J. and Stursberg O. (1999). Verification of logic controller for continuous plants using timed condition/event- system models. Automatica. 35(3): pp. 505-518. T., Moor, and Raisch, J. (2002). Abstraction based supervisory controller synthesis for high order monotone continuous systems. LNCIS 279: pp. 247-265. J. Lunze (1999). A timed discrete-event abstraction of the continuous variable systems. International Journal of Control, 72(13), pp. 1147-1164. H.L. Smith (1995). Monotone dynamical systems: An introduction to the theory of competitive and cooperative systems. Mathematical Surveys and Monographs. 41. 174 p. J.-P. Steyer, Bouvier J.-C., Conte T., Gras P. and Sousbie P. (2002). Evaluation of a four year experience with a fully instrumented anaerobic digestion process. Water Science and Technology. 45(4-5): pp. 495-502. P. Struss (2002). Automated Abstraction of Numerical Simulation Models - Theory and Practical Experience. in Model Based Systems and Qualitative Reasoning for Intelligent Tutoring Systems. San Sebastian (Spain). pp. 161-168. P. Supavatanakul, Falkenberg C. and Lunze J. (2003). Identification of timed discrete event models for diagnosis. In Proc. DX-2003 14th International Workshop on Principles of Diagnosis. Washington DC (USA). S. Yovine (1997). Kronos: A verification tool for real-Time Systems. Journal of Software Tools for Technology Transfer. 1(1-2): pp. 123-133.