Susanna Donatelli
email: donatelli@di.unito.it

Serge Haddad
email: haddad@lsv.fr

Autonomous Transitions Enhance CSL TA Expressiveness and Conciseness

Keywords: 2012 ACM Subject Classification Formal languages and automata theory -Quantitative automata Timed Automata, Markov Chain, Expressiveness Digital Object Identifier 10.4230/LIPIcs

CSL TA is a stochastic temporal logic for continuous-time Markov chains (CTMC) where formulas similarly to those of CTL ˚are inductively defined by nesting of timed path formulas and state formulas. In particular a timed path formula of CSL TA is specified by a single-clock Deterministic Timed Automaton (DTA). Such a DTA features two kinds of transitions: synchronizing transitions triggered by CTMC transitions and autonomous transitions triggered by time elapsing that change the location of the DTA when the clock reaches a given threshold. It has already been shown that CSL TA strictly includes stochastic logics like CSL and asCSL. An interesting variant of CSL TA consists in equipping transitions rather than locations by boolean formulas. Here we answer the following question: do autonomous transitions and/or boolean guards on transitions enhance expressiveness and/or conciseness of DTAs? We show that this is indeed the case. In establishing our main results we also identify an accurate syntactical characterization of DTAs for which the autonomous transitions do not add expressive power but lead to exponentially more concise DTAs.

Introduction

Stochastic logics like CSL [START_REF] Aziz | Model-checking continuoustime Markov chains[END_REF] allow to express assertions about the probability of timed executions of Continuous Time Markov Chains (CTMC). In CSL model executions (typically called "paths") are specified by two operators: timed neXt and timed Until. CSL has been extended in several ways that include action names (name of the events in the paths) and path properties specified using regular expressions leading to asCSL [START_REF] Baier | Model Checking Markov Chains with Actions and State Labels[END_REF], or rewards, leading to CSRL [START_REF] Baier | On the Logical Characterisation of Performability Properties[END_REF]. Note that asCSL can specify rather complex path behaviour, expressed by regular expressions, but the timing requirements cannot be mixed within these expressions. GCSRL [START_REF] Kuntz | GCSRL-a logic for stochastic reward models with timed and untimed behaviour[END_REF] is an extension of CSRL for model checking of CTMC generated by Generalized Stochastic Petri nets (GSPN) [START_REF] Ajmone-Marsan | Modelling with Generalized Stochastic Petri Nets[END_REF] taking into account both stochastic and immediate events.

Automata with time constraints have been used to specify path-based performance indices [START_REF] Obal | State-space support for path-based reward variables[END_REF] for Stochastic Activity Networks [START_REF] Meyer | Stochastic activity networks: Structure, behavior, and application[END_REF], while hybrid automata have been used to define rather complex forms of passage time [START_REF] Elvio | Expressing and computing passage time measures of GSPN models with HASL[END_REF] for GSPN, as well as generic performance properties [START_REF] Ballarini | HASL: A new approach for performance evaluation and model checking from concepts to experimentation[END_REF] that are estimated using simulation. The use of a Deterministic Timed Automaton (DTA) in the stochastic logic CSL TA [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF] allows to specify paths in terms of state propositions and action names associated to CTMC states and transitions (respectively) and in terms of the timed behaviour of portions of the paths. The CTMC actions are the input symbols for the DTA, and two types of transitions are distinguished: synchronizing transitions that read the input symbols of the CTMC, and autonomous transitions, that are taken by the DTA when the clock reaches some threshold. Autonomous transitions have priority over synchronizing ones. The determinism requirement is introduced so that the synchronized product of the DTA and the CTMC is still a stochastic process as all sources XX:2 Autonomous Transitions Enhance CSL TA Expressiveness and Conciseness of non-determinism are eliminated. Furthermore the single clock restriction implies that this stochastic process is a Markov Regenerative Process whose performance indice related to the satisfaction of the formula can be efficiently computed [START_REF] Amparore | Efficient model checking of the stochastic logic cslta[END_REF][START_REF] Elvio | MC4CSL TA : an efficient model checking tool for CSL TA[END_REF]. It has been shown [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF] that CSL TA strictly includes stochastic logics like CSL and asCSL. Various extensions of CSL TA have been presented in the literature. DTA with multiple clocks has been introduced [START_REF] Chen | Model checking of continuous-time Markov chains against timed automata specifications[END_REF].

In that paper a different definition of DTA is used: the state labels of the CTMC act as input symbols of the DTA and autonomous transitions are not considered. The work in [START_REF] Mikeev | On-the-fly verification and optimization of DTA-properties for large Markov chains[END_REF] addresses the model checking of single-clock CSL TA in the context of infinite state Markov chains. The definition of DTA differs from the ones in [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF] and in [START_REF] Chen | Model checking of continuous-time Markov chains against timed automata specifications[END_REF]. Autonomous transitions and actions are not considered and each DTA transition has an associated pair of boolean guards (pre and post). The transition can then be taken only when the CTMC moves from a state that satisfies pre to a state that satisfies post. Our contributions. This paper addresses two research questions aimed at investigating whether there are substantial differences in the various definitions of CSL TA . The first one is whether the presence of autonomous transitions enhances the conciseness and expressiveness of DTAs both in terms of timed languages (qualitative comparison) and in terms of probability of accepting the random path of a CTMC (quantitative comparison). We establish that autonomous transitions with reset do enhance expressiveness, and provide an hierarchy of subclasses of DTA that do not extend expressiveness. We show that w.r.t. conciseness some subclasses are equivalent, while eliminating autonomous transitions from the larger subclass leads to an exponential increase in DTA size. The increase of expressive power has been proved in the less discriminating situation of quantitative comparison (it is indeed possible that two DTAs with different timed languages have the same probability of accepted paths for all Markov chains). This result uses Laplace transforms (often applied to simplify computations) which, to our knowledge, have never been considered for proofs of expressiveness.

The second question is whether the use of boolean guards may change the above set of results. We show that, whatever the considered subclass, DTA with boolean guards are exponentially more concise than DTA with location formulas. Then we prove that all expressiveness results are preserved but one of the transformation with exponential blow-up can now be performed with a polynomial blow-up. This last point requires the use of decision diagrams to represent formulas in the transformed DTA.

The paper is organized as follows: Section 2 introduces the necessary background and the required definitions. Section 3 answers the first research question and Section 4 the second one. Section 5 summarizes the results and outlines practical implications and possible investigations. All proofs not in the text are collected in the appendix.

Context and definitions

Although our motivations rely on the acceptance of paths of CTMCs featuring atomic propositions that label states and actions that label transitions, we set our work in the general context of acceptance of timed paths, where the i `1-th state of a timed path is identified by v i (we count indices from 0), the boolean evaluation of the atomic propositions in that state. δ i indicates a delay, or a sojourn time in state i, and τ i to indicate the time elapsed until exiting state i. A timed path leaves state v i with action a i after a sojourn time in the state equal to δ i . The elapsed time can be computed as: τ i " δ i `τi´1 , with τ ´1 " 0. § Definition 1 (Timed Path). Given a set AP of atomic propositions and a set Act of actions, a timed (infinite) path is a sequence pv 0 , δ 0 q a0 Ý Ñ pv 1 , δ 1 q a1 Ý Ñ ¨¨¨pv i , δ i q ai Ý Ñ ¨¨¨such that for all i P N : v i P tJ, Ku AP , a i P Act, δ i P R ě0 . § Example 2 (Timed path). In writing timed paths we indicate functions v i as the set of elements in AP that evaluate to J. Given AP " tp, qu and Act " ta, b, cu a timed path ptp, qu, 0.5q a Ý Ñ ptqu, 1.3q b Ý Ñ ¨¨¨, is interpreted as the system staying in a state that satisfies p ^q in the time interval r0, 0.5r, at time 0.5 action a takes place and the system moves to a state that satisfies p ^q, stays there for 1.3 time units and then action b takes place (at the global time τ " 1.8).

DTA definition includes a clock x and two types of constraints: boundary ones, BoundC = tx " α, α P Nu and inner ones, InC = tα ' x ' 1 βu, with ', ' 1 P tă, ď, u, α P N, and β P N Y t8u. In the sequel, C is the largest time constant occurring in a DTA.

Before formally defining the syntax and semantic of a DTA (definitions 3, 5 and 7), let us introduce its main ingredients. During the execution of a stochastic discrete event system (e.g. a Markov chain) that can be represented by a timed path, the current location, say , is matched with the current state of the system, say pv i , δ i q. The mapping Λ restricts the possible matchings since the valuation v i must satisfy the formula Λp q. This matching evolves in three ways depending on the delay δ i , elapsed until the next transition pv i , δ i q ai Ý Ñ pv i`1 , δ i`1 q of the system.

Either after some delay δ ď δ i , there is an outgoing autonomous transition from whose boundary condition (say x " α) is satisfied and such that v i fulfills Λp 1 q where 1 is the target location of the transition. Then after delay δ, 1 is matched with s and delay δ i is decreased by δ. Else if there is a synchronizing transition outgoing from such that (1) after time δ i has elapsed its inner condition (say α ' x ' 1 β) is satisfied, (2) the action a belongs to the subset of actions associated with the synchronizing transition, and (3) v i`1 satisfies Λp 1 q where 1 is the target location of the transition Then after delay δ i , 1 is matched with s 1 . Otherwise there is no possible matching and the timed path is rejected by the DTA.

When a transition of the DTA is fired, clock x may keep its current value or may be reset. In the first two cases above, when 1 " f , the final location, the timed path is accepted by the DTA whatever its future. This is ensured due to Λp f q " J and the existence of the unique (looping) synchronizing transition from f with no timing and action conditions. Observe that the synchronization must last forever without visiting f : in this case the timed path is rejected.

Furthermore the synchronization of the stochastic system with the DTA should not introduce non determinism. So (1) the formulas associated with the initial locations are mutually exclusive, (2) synchronizing transitions outgoing from the same location are never simultaneously enabled, (3) autonomous transitions outgoing from the same location are never simultaneously enabled, and (4) autonomous transitions have priority over synchronizing transitions. § Definition 3 (DTA). A single-clock Deterministic Timed Automaton with autonomous transitions is defined by a tuple A " xL, Λ, L 0 , f , AP, Synch, Auty where L is a finite set of locations, L 0 Ď L is the set of initial locations, f P L is the final location, Λ : L Ñ B AP is a function that assigns to each location a boolean expression over the set of propositions AP, Synch Ď L ˆInC ˆ2Act ˆ H, Ó ( ˆL is the set of synchronizing transitions, and Aut Ď L ˆBoundC ˆ7ˆ H, Ó ( ˆL is the set of autonomous transitions, with E " Synch Y Aut.

γ,B,r ÝÝÝÑ 1 denotes the transition p , γ, B, r, 1 q. Furthermore A fulfills the following conditions. Initial determinism. @ , 1 P L 0 , Λplq ^Λpl 1 q ô K.

Determinism on action

. @B, B 1 Ď Act s.t. B X B 1 ‰ H, @ , 1 , 2 P L, if γ,B,r ÝÝÝÑ 1 and γ 1 ,B 1 ,r 1
Ý ÝÝÝÝ Ñ 2 then Λp 1 q ^Λp 2 q ô K or γ ^γ1 ô K. Determinism on autonomous transitions. @ , 1 , 2 P L, if

x"α,7,r Ý ÝÝÝÝ Ñ 1 and

x"α 1 ,7,r 1 Ý ÝÝÝÝÝ Ñ 2 then Λp 1 q ^Λp 2 q ô K or α ‰ α 1 . Conditions on f . Λp f q " J and p f , J, Act, H, f q P Synch.

Given a clock constraint γ and a clock valuation x, x |ù γ denotes the satisfaction of γ by x. Similarly given a boolean formula ϕ and a valuation of atomic propositions v, v |ù ϕ denotes the satisfaction of ϕ by v. Figure 1, left, shows a DTA with five locations: 0 , 1 , 2 , 3 and f . There is a single initial location, 0 . Autonomous transitions are depicted as dotted arcs, while synchronizing are depicted as solid arcs. For readability and conciseness we omit in the drawings: 1) the symbol 7 on autonomous transitions; 2) the set r when there is no reset; 3) Act if a transition accepts all actions; 4) trivially true guards (like x ě 0) and boolean conditions ; 5) the name x of the clock in x " α guards. As a result an autonomous transition is depicted as either l α,Ó Ź l 1 , as between 1 and 0 , or as l α Ź l 1 , as between 0 and 2 . We informally write "a transition with reset" or "a transition without reset" to indicate the condition r "Ó and r " H respectively. The arc from 0 to 1 represents a synchronizing transition with a clock reset. The arc from 0 to 2 represents an autonomous transition to be taken when the clock is equal to 1, with no clock reset. Boolean expression of locations are: p, associated with 0 , 1 , 2 and p p ^qq, associated with 3 .

p 0 p 1 p 2 p ^q 3 f p 0 p ^ q 1 q 2 f x ď 1; aÓ 1Ó b 1 c 2 d x ď 3 α α x ď β x ď β
Let us describe a possible run of this DTA. At time 0.5, it goes from 0 to 1 by performing action a and resets x. Then at time 1.5, it autonomously comes back to location 0 and clock x is again reset. Then it autonomously goes to 2 at time 2.5 and later to f at time 3.5. While irrelevant, x has current value 2.

Figure 1 also shows, on the right, the DTA for the CSL timed-bounded Until pU rα,βs q.

Readers familiar with the definition of DTAs in [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF] may have recognized that the above definition has been slightly changed. Apart from some syntactical changes, the only difference is that we allow cycles made only of autonomous transitions. This restriction was imposed in [START_REF] Donatelli | Model checking timed and stochastic properties with CSL TA[END_REF] to ease the model-checking procedure implementation. § Definition 5 (Run of A). A run of a DTA A is a sequence: p 0 , v 0 , x0 , δ 0 q γ0,B0,r0

ÝÝÝÝÝÑ p 1 , v 1 , x1 , δ 1 q ¨¨¨p i , v i , xi , δ i q γi,Bi,ri Ý ÝÝÝÝ Ñ ¨¨¨such that for all i P N: i P L, 0 P L 0 , v i P tJ, Ku AP , δ i P R ě0 , i γi,Bi,ri Ý ÝÝÝÝ Ñ i`1 P E , v i |ù Λp i q , xi `δi |ù γ i , xi`1 " # 0 if r "Ó
xi `δi otherwise To enforce priority of autonomous transitions, let x7 " mintα | D i x"α,7,r Ý ÝÝÝÝ Ñ P E ^x i ď α ^vi |ù Λp qu (minpHq " 8) If B i " 7 then xi `δi " x7 and v i`1 " v i else xi `δi ă x7 . § Example 6 (DTA run). In the run we, again, describe v in terms of the subset of AP that evaluate to J. For the left DTA of Figure 1 the following is a possible run: p 0 , tpu, x0 " 0.0, δ 0 " 0.2q Ý ÝÝÝÝÝ Ñ p 1 , tp, qu, 0.0, 1.0q

x"1,7,Ó Ý ÝÝÝÝ Ñ p 0 , tp, qu, 0.0, 1.0q

x"1,7,H Ý ÝÝÝÝ Ñ p 2 , tp, qu, 1.0, 0.0q xě0,tcu,H Ý ÝÝÝÝÝÝ Ñ p 0 , tp, qu, 1.0, 0.0q ¨¨Ä timed path σ is recognized by a run ρ of A such that the occurrences of the actions in σ are matched by the synchronizing transitions in ρ. This requires to define a mapping to "couple" the points in the paths in which synchronizing transitions take place. This can be done by identifying a strictly increasing mapping for the indices of the timed path σ to the subset of the indices of the run ρ that correspond to a synchronizing transition. § Definition 7 (Path recognized by A and LpAq ). Let σ " pv 0 , δ 0 q

a0 Ý Ñ pv 1 , δ 1 q a1 Ý Ñ ¨¨¨pv i , δ i q ai Ý Ñ ¨¨¨be a timed path and ρ " p 0 , v 1 0 , x0 , δ 1 0 q γ0,B0,r0 ÝÝÝÝÝÑ ¨¨¨p i , v 1 i , xi , δ 1 i q γi,Bi,ri
Ý ÝÝÝÝ Ñ ¨¨¨be a run of a DTA A. Then σ is recognized by ρ if there is a strictly increasing mapping κ : N Ñ N (extended to κp´1q " ´1q, such that for all i P N a i P B κpiq and δ i " ř κpi´1qăhďκpiq δ 1 h @h, κpi ´1q ă h ď κpiq ñ v 1 h " v i and h R κpNq ñ B h " 7 A timed path σ is accepted by A if σ is recognized by a run ρ and ρ visits f . The language LpAq of A is the set of the timed paths σ accepted by A. :pp, δq ¨¨¨is recognized by the DTA on the right of Figure 1, assuming α " 2 and β " 5, through the run ρ " 0:p 0 , tp, qu, x0 " 0.0, δ 0 " 0.5q Act Ý Ý Ñ 1:p 0 , p, 0.5, 0.6q Act Ý Ý Ñ 2:p 0 , tp, qu, 1.1, 0.9q

x"2,7,H Ý ÝÝÝÝ Ñ 3: p 2 , tp, qu, 2.0, 3.1q Act Ý Ý Ñ 4:p f , p, 5.1, δq ¨¨T he mapping κ fulfills κp0q " 0, κp1q " 1, κp2q " 3, κp3q " 4, . . . Since f is visited by this run, the path is accepted.

DTA have been used to identify sets of behaviours of Continuous Time Markov Chains (CTMCs) that satisfy path formulas of CSL TA , as recalled in the introduction. We shall consider CTMCs in which states are associated with a valuation of a set of propositions AP and a change of states is associated with some actions in Act. This leads to the following representation for CTMCs. § Definition 9 (CTMC representation). A continuous time Markov chain with state and action labels is represented by a tuple M " xS, s 0 , Act, AP, lab, Ry, where S is a finite set of states, s 0 P S the initial state, Act is a finite set of action names, AP is a finite set of atomic propositions, lab : S Ñ tJ, Ku AP is a state-labeling function that assigns to each state s a valuation of the atomic propositions, R Ď S ˆAct ˆS Ñ R ě0 is a rate function. If λ " Rps, a, s 1 q ^λ ą 0, we write s a,λ

Ý Ý Ñ s 1 .
We assume that each state has at least one successor: for all s P S, there exists a P Act, s 1 P S such that Rps, a, s 1 q ą 0. CTMC executions lead to timed paths, and a CTMC is a generator of a random path. We define by Pr M pAq the probability that the random path of M is accepted by A (probability measure of all paths accepted by A as defined in [START_REF] Baier | Model-Checking Algorithms for Continuous-Time Markov Chains[END_REF]).

A denotes the whole family of automata of Definition 3. We identify several subclasses of A, characterized by either the absence of autonomous transitions (A na ) or to a limited presence of such transitions (A nc Ď A nar Ď A rc ), as follows: Restricted cycles A rc is the subclass of automata A P A in which all cycles of A including an autonomous transition with a reset also includes a synchronizing transition p , γ, B, r, 1 q with r "Ó or γ " px ą Cq. No reset on autonomous transitions A nar is the subclass of automata A P A rc in which there is no autonomous transition that resets the clock: A nar " tA P A | p , γ, 7, r, 1 q P AutpAq ñ r " Hu.

No reset and no cyle of autonomous transitions A nc is the subclass of the automata A P

A nar in which there is no cycle made only of autonomous transitions. No autonomous transitions A na is the subclass of the automata A P A nc with no autonomous transitions: A na " tA P A | AutpAq " Hu The DTA on the left of Figure 1 belongs to A rc zA nar , while the one on the right belongs to A nc zA na . Any DTA with no reset on autonomous transitions but with a cycle of autonomous transitions is an example of A nar zA nc .

Let us explain why we introduce the intermediate subclasses between A and A na . A rc points out which syntactical restrictions must be satisfied by automata in A in order to not extend the expressive power of A na . A nar which forbids the clock reset by automous transitions disables the capacity to combine time constants depending on the execution.

A nc which in addition forbids loops of autonomous translations is mainly introduced for simplifying the translations as we will show that it is equivalent to A nar w.r.t. conciseness.

The role of autonomous transitions

We aim at comparing the expressive power of the families of DTA introduced above. We adopt both qualitative and quantitative points of view. From a qualitative point of view, we consider the timed path languages that they generate. From a quantitative point of view, we consider the accepting probabilities associated with the Markov chains. § Definition 10. Let A 1 and A 2 be families of DTA. Then:

A 2 is at least as expressive as A 1 w.r.t. language, denoted A 1 ă L A 2 , if for all A 1 P A 1 there exists A 2 P A 2 such that LpA 2 q " LpA 1 q;
A 2 is at least as expressive as

A 1 w.r.t. Markov chains, denoted A 1 ă M A 2 , if for all A 1 P A 1 there exists A 2 P A 2
such that for all Markov chain M, Pr M pA 2 q " Pr M pA 1 q.

As usual, we derive other relations between such families. A 1 and A 2 are equally expressive w.r.t. language (resp. Markov chains), denoted

A 1 " L A 2 (resp. A 1 " M A 2 ) if A 1 ă L A 2 and A 2 ă L A 1 (resp. A 1 ă M A 2 and A 2 ă M A 1 ). A 2 is strictly more expressive than A 1 w.r.t. language (resp. Markov chains), denoted A 1 ň L A 2 (resp. A 1 ň M A 2 ) if A 1 ă L A 2 and not A 2 ă L A 1 (resp. A 1 ă M A 2 and not A 2 ă M A 1 ). Observe that by definition A 1 ă L A 2 implies A 1 ă M A 2 .
The following frame summarizes the results of this section. The expressiveness results are the strongest possible as the equivalences are proved for the qualitative relation while the strict relation is established for the quantitative relation.

A na " L A nc " L A nar " L A rc ň M A with A rc (resp. A nc ) exponentially more concise than A nar (resp. A na )
and a quadratic translation from A nar to A nc .

' Relation between A and A na .

First we establish that autonomous resetting transitions extend the expressive power of DTA w.r.t. Markov chains. The weaker result w.r.t. language is shown in the appendix since the associated proof is considerably simpler.

To this aim, we establish a kind of 0-1 law for DTA in A na and Markov chains. In order to obtain this intermediate result, we introduce some objects. Simple chains are Markov chains with a single action, no atomic proposition (or equivalently with the same valuation for all states) and such that each state s has a single successor state scpsq reached with rate λ s . W.r.t. the acceptance probability of simple chains, we can consider DTAs without actions and atomic propositions. Moreover we add to each DTA an additional garbage location and we split the transitions, so that, w.l.o.g. one can assume that for each location of a DTA in A na , there are C `1 outgoing transitions:

t i´1ďxăi,ri ÝÝÝÝÝÝÝÑ sc i p q | 1 ď i ď Cu Y t xěC,r C`1 ÝÝÝÝÝÝÑ sc C`1 p qu
where C is the maximal constant occurring in the DTA. The shape of the guards is not a restriction in the context of Markov chains. For all clock valuation x, the clock valuation scp , xq is defined by: Let i " minpj | j P t1, . . . , Cu ^x ă jq with minpHq " C `1; If r i "Ó then scp , xq " 0 else scp , xq " x. Observe the difference between sc i , defined at the syntactical level, which maps a location to its i th successor and sc, defined at the semantical level, which maps a pair consisting in a location and a clock valuation to the new clock valuation obtained by firing the single transition enabled w.r.t. the clock valuation.

We also define the region (multi-)graph G " pV, Eq of such DTA as follows.

V , the set of vertices, is defined by V " tp , iq | P L ^0 ď i ď C `1u; Let p , iq be a vertex, then for all j s.t. maxpi, 1q ď j ď C `1, there is a transition from p , iq to psc j p q, j 1 q labelled by j with j 1 " 0 if r j "Ó and j 1 " j otherwise. One interprets G as follows. The vertex p , 0q corresponds to the region defined by location with clock valuation 0. The vertex p , 1q corresponds to the region defined by location with clock valuation in s0, 1r. The vertex p , iq for 1 ă i ď C corresponds to the region defined by location with clock valuation in ri ´1, ir. The vertex p , C `1q corresponds to the region defined by location with clock valuation in rC, 8r. The transition outgoing from p , iq labelled by j corresponds to the combination of time elapsing to enter the region p , jq followed by an action of the Markov chain, leading to either p 1 , jq or to 1 , 0q, in case of reset.

Given s a state of a Markov chain, a location of DTA, and x a clock valuation, pps, , xq denotes the probability of acceptance when the Markov chain starts in s and the DTA starts in with clock valuation x. In particular for a DTA A applied to a Markov chain M, Pr M pAq " pps 0 , 0 , 0q where s 0 is the initial state of M and 0 is the initial location of A such that labps 0 q |ù Λp 0 q. § Lemma 11. Let s be a state of a simple Markov chain M and be a location of a DTA in A na . Then the function that maps t to pps, , tq is continuous and for i ´1 ď t ď i ď C it is equal to:

ż i t
λse ´λspτ ´tq ppscpsq, sc i p q, scp , τ qqdτ `ż 8 C λse ´λspτ ´tq ppscpsq, sc C`1 p q, scp , τ qqdτ `ÿ iăjďC ż j j´1 λse ´λspτ ´tq ppscpsq, sc j p q, scp , τ qqdτ (1) § Proposition 12. Let A P A na and z P r0, 1s such that for all Markov chain M, Pr M pAq " z then z P t0, 1u.

Proof. We will even prove this result when restricting the quantification to Markov chains with a single action and a single valuation of propositions for all states and a single successor for all states. Thus we can omit propositions and actions in the DTA and only consider simple chains. Let A be an automaton that satisfies the hypothesis. We want to establish that for all configuration p , tq in some region of A reachable from p 0 , 0q, and for all states s of a simple Markov chain pps, , tq " z. We do this by induction on the transition relation of the region graph and then we prove that z is either 0 or 1. The base case of the induction corresponds to the assumption Pr M pAq " z, for all M. For the inductive step we assume that for a given p , tq, and for all states s of a simple chain, pps, , tq " z and we prove that the pps 1 , 1 , t 1 q " z, for all ps 1 1 , t 1 q reachable in one step from ps, , tq. Let M be an arbitrary simple chain and define M λ as the simple chain with a single transition outgoing from its initial state to the initial state of M whose rate is λ. Let s be the initial state of M λ . By assumption, pps, , tq " z. Define f pτ q by ppscpsq, sc j p q, scp , t `τ qq when j ´1 ă t `τ ď j ď C and by ppscpsq, sc C`1 p q, scp , t `τ qq when t `τ ą C. Equation 1 can be rewitten as pps, , tq " ş τ ě0 λe ´λτ f pτ qdτ . Since for all λ, Pr M λ pAq " z, the Laplace transform of f pτ q is equal to z λ , i.e. the Laplace transform of the constant function z. By the theorem of unicity of Laplace transforms, this entails that f pτ q " z except for a set of null measure. However consider a successor region p 1 , iq of location with clock valuation t 1 . ' Either i " 0 (meaning that there has been a reset) and the region has a single point reached with non null probability. So ppscpsq, 1 , 0q " z. ' Or i ą 0, so by Lemma 11, ppscpsq, 1 , t 1 q is continuous inside the region w.r.t. t 1 and thus everywhere equal to z. So the induction is established. So if a region of f is reachable in the region graph z " 1. Otherwise f is not reachable implying that no run is accepting and thus z " 0.

đ

We now establish that A na ň M A. § Proposition 13. There exists A P A such that for all A 1 P A na there exists a Markov chain M with Pr M pA 1 q ‰ Pr M pAq.

Proof.

A described below is associated with an action set reduced to a singleton tau (omitted in the figure) and an empty set of propositions. The language of A is the set of timed paths whose first action occurs at time τ P r2i, 2i `1r for some i P N. Assume by contradiction that there exists A 1 P A na such that for all Markov chain M, Pr M pA 1 q " Pr M pAq.

x ă 1

2Ó

Pick an arbitrary Markov chain M and define M λ as the Markov chain which has a single transition from its initial state to the initial state of M with rate λ. It is routine to check that Pr M λ pAq " 1´e ´λ 1´e ´2λ (as only the first transition of M λ is relevant) and, consequently, lim λÑ0 Pr M λ pAq " 1 2 and, given the hypothesis, also lim λÑ0 Pr M λ pA 1 q " 1 2 . Pr M λ pA 1 q can be decomposed as p 1,λ `p2,λ where p 1,λ is the probability to accept the random timed path and that the first action takes place at most at time C and p 2,λ is the probability to accept the random timed path and that the first action takes place after C, where C is the maximal constant of A 1 . But lim λÑ0 p 1,λ " 0 and therefore lim λÑ0 p 2,λ " 1 2 . On the other hand, let 1 be the location of A 1 reached from its initial location when the value of the clock is greater than C, its maximal constant. There must be one, if not lim λÑ0 p 2,λ " 0, which contradicts what derived above. We want to design an automaton A 2 equivalent to A 1 when reaching 1 with clock value greater than C: any timed path is accepted by A 2 iff it is accepted by A 1 when starting in 1 with clock valuation greater than C. For the construction we duplicate the automaton and merge the final location, the initial location is location 1 of the first copy, and in the first copy we add to the guard of all transitions the formula x ą C and redirect the transitions that reset the clock to the corresponding location of the second copy.

But then lim λÑ0 p 2,λ " Pr M pA 2 q. Since lim λÑ0 p 2,λ " 1 2 and M is arbitrary, this contradicts Proposition 12 applied to A 2 . đ ' From A rc to A na .

We introduced the family A rc to provide an accurate syntactical characterization of DTA for which the autonomous transitions do not add expressive power. In some sense, the DTA of Proposition 13 emphasizes the interest of A rc since the cycle performed by the autonomous resetting transition points out what increases the expressive power. As a first step in the other direction, we establish that in A rc the autonomous resetting transitions can be mimicked using additional finite memory. § Proposition 14. There exists an algorithm operating in exponential time that takes as input A P A rc and outputs A 1 P A nar with LpA 1 q " LpAq.

We illustrate this transformation on the DTA presented on the left of Figure 1 producing the DTA of Figure 2. Here it is sufficient to duplicate once every location. The resetting autonomous transition from 1 to 0 does not reset anymore and goes from x 1 , 0y to x 0 , 1y. The synchronized resetting transition from 0 to 1 yields two transitions from x 0 , iy to x 1 , 0y for i P t0, 1u. The timed constants occurring in the transitions from some x , 1y are increased by 1. The location x 1 , 1y is not present since unreachable from x 0 , 0y. The exponential blowup due to the duplication of locations is unavoidable: § Proposition 15. There exists a family tA n u nPN in A rc such that the size of A n is Opn 2 q and for all A P A nar with LpAq " LpA n q, p|Aut| `1q|Synch| ě 2 n .

In order to eliminate cycles of autonomous transitions of a DTA in A nar , we also add to locations a finite memory representing the number of autonomous transitions visited since the last visit of a synchronized transition. The idea of this construction is that if a path exceeds the number of autonomous transitions it must visit twice the same autonomous transition without visiting a synchronized transition and so diverges. In words: in the resulting DTA, divergence has been transformed into deadlock. This finite memory has a linear size w.r.t. the size of the original DTA. § Proposition 16. There exists an algorithm operating in quadratic time that takes as input A P A nar and outputs A 1 P A nc with LpA 1 q " LpAq.

We show how to eliminate autonomous transitions without reset (that do not form a cycle). The key point is to select a location which is the source of the last autonomous transition of a maximal path of such transitions. Thus every autonomous transition outgoing from reaches some location u where only synchronized transitions are possible. Roughly speaking, the construction builds a synchronized transition corresponding to a sequence of an autonomous transition followed by a synchronized transition. However the construction is more involved since has to be duplicated in order to check which autonomous transition can be triggered (or if no autonomous transition can be triggered). This duplication has also an impact on the incoming transitions of . Repeating (at most |L| times) this transformation eliminates all autonomous transitions. In appendix, we illustrate this transformation on the DTA presented on the right of Figure 1. § Proposition 17. There exists an algorithm operating in exponential time that takes as input A P A nc and outputs A 1 P A na with LpA 1 q " LpAq.

The exponential blowup due to the repetition of duplication of locations is unavoidable as shown by the next proposition. § Proposition 18. There exists a family of automata tA n u nPN in A nar such that the size of A n belongs to Opn logpnqq and for all A P A na with LpAq " LpA n q the number of its locations is at least 2 n .

DTA with boolean guards

An alternative version of DTA has been proposed in [START_REF] Mikeev | On-the-fly verification and optimization of DTA-properties for large Markov chains[END_REF]

As before

ϕ ´,γ,B,r,ϕ Ý ÝÝÝÝÝÝÝ Ñ 1 denotes the synchronized transition p , ϕ ´, γ, B, r, ϕ `, 1 q. and ϕ ´,γ,7,rp,ϕ ´q Ý ÝÝÝÝÝÝÝÝ Ñ 1 (repeating sometimes the formula for unifying the notations) denotes the autonomous transition p , ϕ ´, γ, 7, r, 1 q. Furthermore A fulfills the following conditions.

Determinism on actions. @B,

B 1 Ď Act s.t. B X B 1 ‰ H, @ , 1 , 2 P L, if ϕ ´,γ,B,r,ϕ Ý ÝÝÝÝÝÝÝ Ñ 1 ^ ϕ 1´, γ 1 ,B 1 ,r 1 ,ϕ 1Ý
ÝÝÝÝÝÝÝÝÝ Ñ 2 then ϕ ´^ϕ 1´ô K or ϕ `^ϕ 1`ô K or γ ^γ1 ô K. Determinism on autonomous transitions. @ , 1 , 2 P L,

if ϕ ´,x"α,7,r Ý ÝÝÝÝÝÝÑ 1 and ϕ 1´, x"α 1 ,7,r 1 ÝÝÝÝÝÝÝÝÑ 2 then ϕ ´^ϕ 1´ô K or α ‰ α 1 .
Condition on the final location. f J,J,Act,H,J ÝÝÝÝÝÝÝÝÑ f P Synch.

One denotes the class of such DTA by A g with subclasses by A na g , A nc g , A nar g and A rc g . § Definition 20 (Run of a DTA).

A run of a DTA A is a sequence: ρ " p 0 , v 0 , x0 , δ 0 q ϕ 0 ,γ0,B0,r0,ϕ

0 Ý ÝÝÝÝÝÝÝÝÝ Ñ p 1 , v 1 , x1 , δ 1 q ϕ 1 ,γ1,B1,r1,ϕ 1 Ý ÝÝÝÝÝÝÝÝÝ Ñ ¨¨¨p i , v i , xi , δ i q ϕ í ,γi,Bi,ri,ϕ ì Ý ÝÝÝÝÝÝÝÝÝ Ñ ¨¨¨such that for all i P N, i P L, v i P tK, Ju AP , δ i P R ě0 , i ϕ í ,γi,Bi,ri,ϕ ì Ý ÝÝÝÝÝÝÝÝÝ Ñ i`1 P E, v i |ù ϕ í , v i`1 |ù ϕ ì , xi `δi |ù γ i , xi`1 " # 0 if r i "Ó xi `δi otherwise Let x7 " mintα | D i ϕ,x"α,7,r
Ý ÝÝÝÝÝ Ñ 1 P E ^x i ď α ^vi |ù ϕu. If B i " 7 then xi `δi " x7 and v i`1 " v i else xi `δi ă x 7 . § Definition 21. Let σ " pv 0 , δ 0 q a0 Ý Ñ pv 1 , δ 1 q a1 Ý Ñ ¨¨¨pv i , δ i q ai Ý Ñ ¨¨¨be a timed path and

ρ " p 0 , v 1 0 , x0 , δ 1 0 q ϕ 0 ,γ0,B0,r0,ϕ 0 Ý ÝÝÝÝÝÝÝÝÝ Ñ ¨¨¨p i , v 1 i , xi , δ 1 i q ϕ í ,γi,Bi,ri,ϕ ì
Ý ÝÝÝÝÝÝÝÝÝ Ñ ¨¨¨be a run of a DTA A. Then σ is recognized by ρ if there is a strictly increasing mapping κ : N Ñ N (extended to κp´1q " ´1q, such that for all i P N:

a i P B κpiq and δ i " ř κpi´1qăhďκpiq δ 1 h ; @h, κpi ´1q ă h ď κpiq ñ v 1 h " v i and h R κpNq ñ B h " 7.
A timed path σ is accepted by A if σ is recognized by a run ρ, and ρ visits f . Our results are summarized below. Let us emphasize the main items: (1) while being equivalent to the original version, this model is exponentially more concise and (2) the elimination of autonomous transitions without reset that was performed in exponential time in the original version is now performed in polynomial time.

A na g " L A nc g " L A nar g " L A rc g ň M A g " L A with A g (resp.
A rc g ) exponentially more concise than A (resp. A nar g ) and a quadratic (resp. polynomial) translation from A nar g (resp. A nc g ) to A nc g (resp. A na g ).

' From A to A g and back. The translation from A to A g mainly consists in shifting the formula of the location to the incoming transitions with a particular handling of the initial locations. § Proposition 22. There exists an algorithm operating in quadratic time that takes as input A P A (resp. A na , A nc , A nar , A rc ) and outputs A 1 P A g (resp. A na g , A nc g , A nar g , A rc g ) with LpA 1 q " LpAq.

The reverse translation is more costly and consists in duplicating a location w.r.t. the guards of the incoming and outgoing transitions. § Proposition 23. There exists an algorithm operating in exponential time that takes as input A P A g (resp. A na g , A nc g , A nar g , A rc g ) and outputs A 1 P A (resp. A na , A nc , A nar , A rc ) with LpA 1 q " LpAq.

The exponential blowup due to the duplication of locations is unavoidable even without timing considerations as shown by the next proposition. § Proposition 24. There exists a family of automata tA n u nPN in A na g such that the size of A n belongs to Opn logpnqq and for all A P A with LpAq " LpA n q the number of its locations is at least 2 n ´1.

' From A rc g to A na g . Since the algorithm of Proposition 14 does not transform the propositional features of the DTA, it is also appropriate for A rc g . Similarly the exponential lower bound still holds. § Proposition 25. There exists an algorithm operating in exponential time that takes as input A P A rc g and outputs A 1 P A nar g with LpA 1 q " LpAq. There exists a family tA n u nPN in A rc g such that the size of A n belongs to Opn 2 q and for all A P A nar g with LpAq " LpA n q, p|Aut| `1q|Synch| ě 2 n .

Since the algorithm of Proposition 16 does not transform the propositional features of the DTA, it is also appropriate for A nar g . § Proposition 26. There exists an algorithm operating in quadratic time that takes as input A P A nar g and outputs A 1 P A nc g with LpA 1 q " LpAq.

An interesting feature of specifying propositional formulas on transitions is that the final transformation can be performed in polynomial time. To this aim we introduce a particular case of decision diagram (DD) for representating formulas as follows. Let DG be a directed acyclic graph rooted in u 0 including a final vertex u f such that all vertices are reachable from u 0 and can reach u f . Every transition is labelled by a formula and the formulas labeling outgoing transitions from a vertex are mutually exclusive. Given a valuation v, v |ù DG if there is a path from u 0 to u f such that v |ù ϕ for all ϕ labeling transition of the path. Observe that there is at most one such path. Thus deciding whether v |ù DG can be performed in linear time (assuming that the satisfaction of a formula labeling a transition by a valuation can be performed in linear time which is the case for standard representation of formulas). So in the next proposition, one assumes that the formulas can be specified with such DD. § Proposition 27. There exists an algorithm operating in polynomial time that takes as input A P A nc g and outputs A 1 P A na g with LpA 1 q " LpAq.

Proof. The transformation proceeds in three stages (exemplified in the appendix) ' The first stage consists in duplicating the locations w.r.t. time regions. Let 0 " α 0 ă . . . ă α m " C be the time constants occurring in A (adding 0 if necessary). The set of time regions is tα 0 u, sα 0 , α 1 r, tα 1 u, . . . , tα m u, sα m , 8r. For all location and all region rg, one creates a location x , rgy. The initial location is x 0 , tα 0 uy with 0 the initial location of A.

For all synchronized transition

ϕ ´,γ,B,r,ϕ Ý ÝÝÝÝÝÝÝ Ñ 1 and all regions rg and rg 1 one creates a transition x , rgy ϕ ´,γ^xPrg 1 ,B,r,ϕ Ý ÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x 1 , rg 1 y. For all autonomous transition ϕ,x"i,7,H

ÝÝÝÝÝÝÑ 1 and all region rg, one creates a transition x , rgy ϕ,x"i,7,H ÝÝÝÝÝÝÑ x 1 , tiuy. ' Let A 1 be the DTA produced by the first stage, the second stage produces a DTA A 2 where the priority of the autonomous transitions is made explicit by restricting the temporal formulas of outgoing transitions. Let x , rgy be a location and tt k " x , rgy ϕ k ,x"α k ,7,H ÝÝÝÝÝÝÝÝÑ x k , tα k uyu kďK be the autonomous transitions outgoing from x , rgy with rg ď α 1 ď ¨¨¨ď α K (the other autonomous transitions are useless and are assumed to be deleted).

For all k, one creates an autonomous transition x , rgy

ϕ k ^Źk 1 ăk ϕ k 1 ,x"α k ,7,H Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x k , tα k uy.
For all synchronized transition x , rgy

ϕ ´,γ,B,r,ϕ Ý ÝÝÝÝÝÝÝ Ñ x 1 , rg 1 y, one creates a transition x , rgy ϕ ´^Ź α k ďrg 1 ϕ k ,γ,B,r,ϕ Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x 1
, rg 1 y. In A 2 disregarding the priority of autonomous transitions does not modify the language. ' The final stage that produces A 1 from A 2 consists in deleting the autonomous transitions and adding new synchronized transitions as follows. For all x , rgy and x 1 , tiuy such that there is a path of autonomous transitions from x , rgy to x 1 , tiuy, one specifies the formula ϕ by a DD whose vertices are locations both reachable from x , rgy by autonomous transitions and can reach x 1 , tiuy by autonomous transitions. The edges of the DD are the autonomous transitions between such vertices labeled by the formulas of the autonomous transitions.

Then for all synchronized transition x 1 , tiuy

ϕ ´,γ,B,r,ϕ Ý ÝÝÝÝÝÝÝ Ñ x 2 , rg 2 y, one creates a transition x , rgy ϕ^ϕ ´,xěi^γ,B,r,ϕ Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x 2 ,
rg 2 y. Then, all locations x f , rgy are merged into a single one. đ

Conclusion and future work

We have established that autonomous transitions do enhance expressiveness of single clock DTAs, and more precisely for the less discriminating case of the probability of the random paths of a CTMC accepted by the DTA. This is the most relevant one for comparing some variations of (1-clock) CSL TA defined in the literature. This enhanced expressiveness is due to the possibility of associating clock resets with autonomous transitions that occur in a cycle. The small counterexample of Proposition 13 can be seen as the basic construct to study systems with periodic behaviours or periodic phases, with clear practical implications. Even in DTA subclasses for which the autonomous transitions do not enhance expressiveness, they do play a role in defining concise DTAs: removing autonomous transitions may lead to an exponential blow up of the DTA. Considering DTAs with boolean guards associated with transitions the effect of the presence of autonomous transitions does not change, but the use of guards may lead to more concise DTAs. We plan to investigate whether the precise identification of the characteristics that enhance expressiveness and conciseness can help the identification of the best algorithms for CSL TA model-checking, in particular for the recently proposed component-based method [START_REF] Amparore | Efficient model checking of the stochastic logic cslta[END_REF].

6 Appendix 6.1 A versus A na § Proposition 28. Let A be the DTA presented in the proof of Proposition 13. There does not exist an automaton A 1 P A na such that LpA 1 q " LpAq.

Proof. Assume by contradiction that there exists A 1 P A na such that LpA 1 q " LpAq.

Let C be the maximal constant occurring in A 1 that we assume w.l.o.g. to be odd. The timed path pC `1q a Ý Ñ p0q a Ý Ñ p0q ¨¨¨a Ý Ñ p0q ¨¨¨belongs to LpAq " LpA 1 q (here we omit the valuation since the set of propositions is empty).

Let p , C `1q γ0,tau,r0 Ý ÝÝÝÝÝ Ñ p 1 , 0q ¨¨¨be the corresponding accepting run.

Then for all τ ą 0, the run p 0 , C `τ q γ0,tau,r0 Ý ÝÝÝÝÝ Ñ p 1 , 0q ¨¨¨is also accepting which entails that the timed path pC `2q a Ý Ñ p0q a Ý Ñ p0q ¨¨¨a Ý Ñ p0q ¨¨¨belongs to LpA 1 q in contradiction with LpA 1 q " LpAq.

đ § Lemma 11. Let s be a state of a simple Markov chain M and be a location of a DTA in A na . Then the function that maps t to pps, , tq is continuous and for i ´1 ď t ď i ď C it is equal to:

ż i t λse ´λspτ ´tq ppscpsq, sc i p q, scp , τ qqdτ `ż 8 C λse ´λspτ ´tq ppscpsq, sc C`1 p q, scp , τ qqdτ `ÿ iăjďC ż j j´1 λse ´λspτ ´tq ppscpsq, sc j p q, scp , τ qqdτ (1)
The above formula computes the probability of acceptance when the Markov chain starts in s and the DTA starts in with clock valuation t, with i ´1 ď t ď i ď C, therefore within the region pl, iq. This probability is computed in terms of the probability of having the next CTMC transition within the region pl, iq itself, or any later region pl, jq, multiplied by the probability of acceptance from the state reached by accepting the CTMC transition.

Proof. Define p n ps, , tq as the probability that the run associated with a random timed path of M starting in s when the DTA starts in with clock valuation t reaches location f after performing n actions. Then for ‰ f , p 0 ps, , tq " 0 and p 0 ps, f , tq " 1. Assume that p n ps, , tq is continuous (and so measurable) for all s and . Then the following equation holds for i ´1 ď t ď i ď C:

p n`1 ps, , tq "

ż i t λ q e ´λspτ ´tq p n pscpsq, sc i p q, scp , τ qqdτ `ÿ iăjďC ż j j´1
λ s e ´λqpτ ´tq p n pscpsq, sc j p q, scp , τ qqdτ `ż 8

C

λ s e ´λspτ ´tq p n pscpsq, sc C`1 p q, scp , τ qqdτ

Observe that for τ ą C, p n pscpsq, sc C`1 p q, scp , τ qq is constant since if there is a reset then scp , τ q " 0 and if there is no reset then scp , τ q " τ ą C and so the valuation of the clock is XX:16 Autonomous Transitions Enhance CSL TA Expressiveness and Conciseness irrelevant. Thus the equation can be rewritten as follows.

p n`1 ps, , tq "

ż i t
λ s e ´λspτ ´tq p n pscpsq, sc i p q, scp , τ qqdτ `ÿ iăjďC ż j j´1 λ s e ´λspτ ´tq p n pscpsq, sc j p q, scp , τ qqdτ `e´λspC´tq p n pscpsq, sc C`1 p q, scp , C `1qq

Observe that maxp1, λ s qe ´λsτ is uniformly continuous. So pick η 1 ą 0 such that for all

τ ă τ 1 ď τ `η1 maxp1, λ s q|e ´λsτ ´e´λsτ 1 | ď ε 3C . Let η " minpη 1 , ε 3λs q.
Then for all t ă t 1 ď t `η, one bounds |p n`1 ps, , tq ´pn`1 ps, , t 1 q| by the sum of three terms using the above equation to establish that |p n`1 ps, , tq ´pn`1 ps, , t 1 q| ď ε. Thus p n`1 ps, , tq is continuous. When t ą C, p n`1 ps, , tq is constant and so continuous. Observe that pps, , tq " lim nÑ8 p n ps, , tq. So the mapping pps, , tq is measurable as a limit of continuous mappings. Thus Equation 1 holds for i ´1 ď t ď i ď C: Repeating the same argument as the one for the inductive case yields the result. When t ą C, pps, , tq is constant and so continuous. đ

6.2 A rc " L A nar " L A nc " L A na § Proposition 14.
There exists an algorithm operating in exponential time that takes as input A P A rc and outputs A 1 P A nar with LpA 1 q " LpAq.

Proof. Consider an elementary path of A not including synchronized transitions with reset or with guard x ą C. Define its delay to be the sum of constants occurring in its autonomous transitions with reset. Let K be the maximal delay of such paths. The set of locations of A 1 is L 1 " tx , iy | 0 ď i ď K ^ P Lzt f uu Y t f u with set of initial locations L 1 0 " tx , 0y P L 1 | P L 0 u and final location f (with its single looping transition). For all x , iy, Λpx , iyq " Λp q. Let γ be a guard. Define γ `i the guard where all constants of γ are increased by i.

For all synchronized transition γ,B,r ÝÝÝÑ 1 ( ‰ f ) of A and i ď K: if 1 " f then there is a synchronized transition x , iy γ`i,B,r Ý ÝÝÝÝ Ñ f ; else if r "Ó or γ " x ą C then there is a synchronized transition x , iy γ`i,B,r Ý ÝÝÝÝ Ñ x 1 , 0y; otherwise there is a synchronized transition x , iy γ`i,B,r Ý ÝÝÝÝ Ñ x 1 , iy. For all autonomous transition

x"c,7,r Ý ÝÝÝÝ Ñ 1 of A and i ď K: if 1 " f then there is an autonomous transition x , iy

x"c`i,7,H Ý ÝÝÝÝÝÝ Ñ f ; else if r " H there is an autonomous transition x , iy

x"c`i,7,H Ý ÝÝÝÝÝÝ Ñ x 1 , iy; else if r "Ó and c `i ď K then there is an autonomous transition x , iy

x"c`i,7,H Ý ÝÝÝÝÝÝ Ñ x 1 , c `iy. Observe that A 1 has no more autonomous transitions with reset. For sake of simplicity, let x f , iy denote f for all i. Let us establish the correctness of this transformation. ' Let ρ " p 0 , v 0 , x0 , δ 0 q γ0,B0,r0 ÝÝÝÝÝÑ p 1 , v 1 , x1 , δ 1 q ¨¨¨γ n´1 ,Bn´1,rn´1 ÝÝÝÝÝÝÝÝÝÝÑ p n , v n , xn , δ n q ¨¨¨be a run of A.

run for σ v 1 up to v 1 " v with clock valuation xv 1 " xv and then going on with the suffix of the accepting run for σ v . However since zpvq ă zpv 1 q such a path does not belong to LpA n q.

đ § Proposition 16. There exists an algorithm operating in quadratic time that takes as input A P A nar and outputs A 1 P A nc with LpA 1 q " LpAq.

Proof. Let A P A nar . Observe that if a timed path visits twice the same autonomous transition without in the meantime visiting a synchronized transition, then it will infinitely cycles visiting only autonomous transitions (i.e. diverging). Let K be the number of autonomous transitions. A 1 is built as follows. The set of locations of

A 1 is L 1 " tp , iq | 0 ď i ď K ^ P Lzt f uu Y t f , K u with set of initial locations L 1
0 " tp , 0q P L 1 | P L 0 u and final location f (with its single looping transition). For all x , iy, Λpx , iyq " Λp q. Λp K q " J.

For all synchronized transition γ,B,r ÝÝÝÑ 1 of A and i ď K: if 1 " f then there is a synchronized transition p , iq γ,B,r ÝÝÝÑ f ; otherwise there is a synchronized transition p , iq γ,B,r ÝÝÝÑ p 1 , 0q. For all autonomous transition

x"c,7,H Ý ÝÝÝÝ Ñ 1 of A and i ď K: if i " K then there is an autonomous transition p , iq

x"c,7,H Ý ÝÝÝÝ Ñ K ; else if 1 " f then there is an autonomous transition p , iq

x"c,7,H Ý ÝÝÝÝ Ñ f ; otherwise there is an autonomous transition p , iq

x"c,7,H Ý ÝÝÝÝ Ñ p 1 , i `1q. By construction, there is no cycle of autonomous transitions in A 1 . A timed path of A 1 that does not visit K provides a timed path of A by omitting the second component of the locations while the only timed paths of A that cannot be mimicked by A 1 are the diverging ones. Furthermore the "partial" simulation of such paths by A 1 leads to a deadlock location.

đ § Proposition 17. There exists an algorithm operating in exponential time that takes as input A P A nc and outputs A 1 P A na with LpA 1 q " LpAq.

Proof. The algorithm iteratively applies a transformation that decreases the number of locations that are sources of autonomous transitions. Let tt u "

x"cu,7

ÝÝÝÝÑ u u uďk be the last transitions of elementary paths consisting of autonomous transitions with maximal length starting from some (there must be at least one such location). W.l.o.g assume that c 1 ď ¨¨¨ď c k . We denote this set of values (adding 0 if necessary) as 0 " α 0 ă ¨¨¨ă α K by eliminating repetitions. By convention, α ´1 " ´8. One builds another A 1 P A nc as follows.

One creates two sets of locations: tx , i, uy | 0 ď i ď K, 1 ď u ď k, α i ď c u u and tx , iy | 0 ď i ď K `1u. The location x , i, uy corresponds to location with additional requirements [START_REF] Ajmone-Marsan | Modelling with Generalized Stochastic Petri Nets[END_REF] to enter in it with clock valuation in sα i´1 , α i s and (2) such that if no synchronized transitions occurs then the autonomous transition t u is followed. For i ď K, the location x , iy corresponds to location with additional requirements [START_REF] Ajmone-Marsan | Modelling with Generalized Stochastic Petri Nets[END_REF] to enter in it with clock valuation in sα i´1 , α i s and (2) such that no autonomous transition can occur. The location x , K `1y corresponds to location with additional requirement to enter in it with clock valuation in sα K , 8r.

For all i, u, Λpx , i, uyq " Λp q ^pŹ αi´1ăa u 1 ăau Λp u 1 qq ^Λp u q; For all i ď K, Λpx , iyq " Λp q ^pŹ αi´1ăa u 1

Λp u 1 qq; Λpx , K `1yq " Λp q.

For all transition ´γ´, B Ý ÝÝÝÑ with ´‰ and all i, u, one creates transitions: For all synchronized transition γ `,B Ý ÝÝÝÑ and all i, i 1 , u, u 1 , one creates transitions: x , i, uy

´γ´^α i´1 ăxďαi,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x , i
γ `^xăcu^α i 1 ´1ăxďα i 1 ,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÑ x , i 1 , u 1 y, x , i, uy γ `^xăcu ^αi´1ăxďαi,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÑ x , i 1 y, x , iy γ `^α i 1 ´1 ăxďα i 1 ,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x , i 1 , u 1 y, x , iy γ `^α i 1 ´1ăxďα i 1 ,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x , i 1 y and x , iy γ `^α K ăx,B Ý ÝÝÝÝÝÝÝÝÑ x , K `1y.
For all synchronized transition γ `,B `,Ó ÝÝÝÝÝÑ and all i, u, u 1 , one creates transitions: x , i, uy For all synchronized transition u γ `,B Ý ÝÝÝÑ and all i, i 1 , u 1 one creates transitions: x , i, uy

γ `^xăcu ,B ´,Ó Ý ÝÝÝÝÝÝÝÝÝ Ñ x , 0, u 1 y, x , i, uy γ `^xăcu,B ´,Ó Ý ÝÝÝÝÝÝÝÝÝ Ñ x , 0y, x , iy γ `,B ´,Ó ÝÝÝÝÝÑ x , 0, u 1 y,
γ `^xěcu ^αi 1 ´1ăxďα i 1 ,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÑ x , i 1 , u 1 y, x , i, uy γ `^xěcu ^αi 1 ´1 ăxďα i 1 ,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÝÑ x , i 1 y and x , i, uy γ `^xěcu ^αK ăx,B Ý ÝÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x , K `1y.
For all synchronized transition u γ `,B `,Ó ÝÝÝÝÝÑ and all i, u 1 one creates transitions: x , i, uy

γ `^xěcu ,B `,Ó Ý ÝÝÝÝÝÝÝÝÝ Ñ
x , 0, u 1 y and x , i, uy γ `^xěcu ,B `,Ó Ý ÝÝÝÝÝÝÝÝÝ Ñ x , 0y. Then we delete and all adjacent transitions. By construction, A and A 1 accept the same timed paths and there is one less location source of an autonomous transition. One can iterate at most |L| times this transformation leading to an equivalent automaton in A na . đ

We illustrate this transformation on the DTA presented on the right of Figure 1 producing the DTA of Figure 3. The only location from which autonomous transitions start is 0 . The autonomous transitions are triggered when x " α and lead to locations with formulas q and p ^ q. Combining them with formula p of 0 entails that 0 has to be duplicated into three locations: (1) 0,0 that must be entered with clock value at most α and with formula p ^ q, (2) 0,1 that must be entered with clock value at most α and with formula p ^q, (3) and another location that must be entered with clock value greater than α and with formula p. However this location is not reachable and so omitted in the figure. The transition looping around 0 yields to four transitions depending on which formulas hold before and after the transition. The transition from 0,0 to 1 corresponds to the sequence of transitions in the original automaton of the autonomous transition from 0 to 1 followed by the synchonized transition which loops around 1 . § Proposition 18. There exists a family of automata tA n u nPN in A nar such that the size of A n belongs to Opn logpnqq and for all A P A na with LpAq " LpA n q the number of its locations is at least 2 n .

Proof. Consider the automaton A n described below. Here Act is a singleton and so we omit the labels of the actions. A n accepts the timed paths where: either there is no action before time n or there is a single action before time n at some time τ with i ď τ ă i `1 ď n and p i initially true. Assume by contradiction that there exists A P A na with LpAq " LpA n q and less than 2 n locations. In particular, it has less than 2 n initial locations. Since there are accepted timed paths for any initial valuation of the atomic propositions, two different valuations (say v and v 1 ) of the atomic propositions should satisfy Λp 0 q for some initial location 0 . Let p i be such that vpp i q " J and v 1 pp i q " K. Any timed path starting with initial valuation v and a single action occurring in r0, nr at some time τ with i ď τ ă i `1 ď n is accepted. This implies that any timed path starting with initial valuation v 1 and a single action occurring in r0, nr at some time τ with i ď τ ă i `1 ď n is also accepted. But such a timed path does not belong to LpA n q. đ 6.3 A versus A g § Proposition 22. There exists an algorithm operating in quadratic time that takes as input A P A (resp. A na , A nc , A nar , A rc ) and outputs A 1 P A g (resp. A na g , A nc g , A nar g , A rc g ) with LpA 1 q " LpAq.

XX:20 Autonomous Transitions Enhance CSL TA Expressiveness and Conciseness

p ^q 0,1 p ^ q 0,0 p ^ q 1 q 2 f α ď x ď β α ď x ď β x ě α x ď β x ď β x ă α x ă α x ă α x ă α
Proof. A 1 has the same structure as A except that it has an additional location 0 which is the initial one. For all synchronized transition γ,B,r ÝÝÝÑ 1 in A, A 1 includes the synchronized transition J,γ,B,r,Λp 1 q ÝÝÝÝÝÝÝÝÑ 1 and if P L 0 then A 1 includes the synchronized transition 0 Λp q,γ,B,r,Λp 1 q Ý ÝÝÝÝÝÝÝÝÝ Ñ 1 . For all autonomous transition

x"α,7,r Ý ÝÝÝÝ Ñ 1 in A, A 1 includes the autonomous transition Λp 1 q,x"α,7,r ÝÝÝÝÝÝÝÝÑ 1 and if P L 0 then A 1 includes the autonomous transition: 0 Λp q^Λp 1 q,x"α,7,r ÝÝÝÝÝÝÝÝÝÝÝÝÑ 1 . The quadratic factor is mainly due to the substitution of |L| formulas by at least |E| formulas. đ § Proposition 23. There exists an algorithm operating in exponential time that takes as input A P A g (resp. A na g , A nc g , A nar g , A rc g ) and outputs A 1 P A (resp. A na , A nc , A nar , A rc ) with LpA 1 q " LpAq.

Proof. Given P L, let ϕ 1 , . . . ϕ n be the formulas of entering guards of transitions incoming and exiting guards of transitions outgoing . Then L 1 " tx , Iy | P L^I Ď t1, . . . , n uuYt f u where f is the final state (fulfilling the requirements of a DTA in A) and for all x , Iy, Λpx , Iyq " Ź iPI ϕ i ^ŹiRI ϕ i .

For all synchronized transition ϕ i ,γ,B,r,ϕ

1 i 1
Ý ÝÝÝÝÝÝÝ Ñ 1 in A 1 and all I, I 1 such that i P I and i 1 P I 1 , A 1 includes the synchronized transition: x , Iy γ,B,r ÝÝÝÑ x 1 , I 1 y. For all autonomous transition ϕ i ,x"α,7,r Ý ÝÝÝÝÝÝ Ñ 1 in A and all I, I 1 such that i P I and i 1 P I 1 with ϕ i " ϕ 1 i 1 , A 1 includes the autonomous transition: x , Iy

x"α,7,r Ý ÝÝÝÝ Ñ x 1 , I 1 y. For all x f , Iy, there is a transition x f , Iy J,Act,H ÝÝÝÝÝÑ f . đ § Proposition 24. There exists a family of automata tA n u nPN in A na g such that the size of A n belongs to Opn logpnqq and for all A P A with LpAq " LpA n q the number of its locations is at least 2 n ´1.

Proof. Consider the automaton A n described below. . . . p 1 , a 1 p n , a n This automaton accepts timed paths whose first action may be a i only if the initial state fullfills p i . Consider in A the locations reached at time 0 by the runs before the first action is performed. At least 2 n ´1 initial valuations must reach such a location. Assume that A has less than 2 n ´1 locations. Then two initial valuations reach the same location. Let p i be some proposition on which they differ. Thus there exists a initial valuation v with vpp i q " K such that a timed path starting with a i is accepted which yields a contradiction. đ 6.4 A rc g " L A nar g " L A nc g " L A na g § Proposition 25. There exists an algorithm operating in exponential time that takes as input A P A rc g and outputs A 1 P A nar g with LpA 1 q " LpAq. There exists a family tA n u nPN in A rc g such that the size of A n belongs to Opn 2 q and for all A P A nar g with LpAq " LpA n q, p|Aut| `1q|Synch| ě 2 n .

Proof. Here we only exhibit the family tA n u nPN . Given A n described below, the proof is done as the one of Proposition 15. p ^ q, α p ^q, α x " α, p ^q x " α, p ^ q α ă x ă β, q x ą α α ă x ă β, p ^ q α ă x ă β, q p, p x " α, p ^ q x " α, p ^q α ă x ă β, p ^ q Figure 4 A DTA specification of pU sα,βr q with α ą 0.

Application of Proposition 27.

The DTA with boolean guards of Figure 4 illustrates how to specify the temporal formula pU sα,βr q with a DTA A P A nc g . Observe that in the interval r0, αr, the current location can only be 0 with the additional requirement that if an action occurs then p has to be fullfilled inside the whole interval. At time α, the current location can only be 1 or 2 depending on the truth value of q and with the guarantee that p holds in the interval r0, αs. Considering the first action that occurs after α, there are three possible cases: (1) either p ^q was satisfied and the formula is satisfied, (2)either p ^ q was satisfied, q is now satisfied and the action occurs before β and so the formula is satisfied (3) or p ^ q was satisfied and is still satisfied and the action occurs before β and so there is the same possibility to satisfy the formula represented by location 3 .

Figure 5 depicts the DTA A 1 P A na g obtained by applying the transformation of Proposition 27 to the DTA A P A nc g depicted in Figure 4. W.r.t. the defined transformation, we have done some simplifications. Since 1 and 2 can only be entered at time α there is no need to duplicate them. Since 3 can only be entered in interval sα, βr there is no need to duplicate it. In addition we have merged x 0 , 0y and x 0 , s0, αry since their outgoing transitions are identical (up to the merging). We have also omitted locations that cannot reach the final location. p, x " α, p ^ q p, x " α, p ^q α ă x ă β, p ^ q p ^q, x ą α p ^ q, α ă x ă β, q

x " α, p ^q x " α, p ^ q α ă x ă β, q x ą α α ă x ă β, p ^ q α ă x ă β, q p, x ă α, p

x " α, p ^ q x " α, p ^q α ă x ă β, p ^ q Figure 5 Another DTA specification of pU sα,βr q with α ą 0.

Figure 1

 1 Figure 1 Two examples of DTA.

  Note that, due to determinism, if such a run exists, it is unique. § Example 8 (Timed path recognized by a DTA run). A timed path σ " pp, 0.2q a Ý Ñ ptp, qu, 0.7q b Ý Ñ pq, 1.0q c Ý Ñ ¨¨¨is recognized in the DTA on the left of Figure 1 by the first run of Example 6, with a one-to-one mapping κ. Since f is visited by this run, σ P LpAq. A timed path σ " 0:ptp, qu, 0.5q a Ý Ñ 1:pp, 0.6q b Ý Ñ 2:ptp, qu, 4.0q c Ý Ñ 3 :

4 Figure 2

 42 Figure 2 Elimination of resetting autonomous transitions.

Figure 3

 3 Figure 3 Elimination of autonomous transitions with no reset.

  : locations have no associated formula, synchronized transitions have two formulas, one evaluated on the source state and one evaluated on the destination state. Autonomous transitions have a formula evaluated in the current state. Our aim is twofold: first relate the two versions w.r.t. expressiveness and conciseness and then examine whether the relations established for the previous case still hold. Let us formalize this model by adapting the definitions of section 2. § Definition 19 (DTA). A DTA with boolean guards is defined by a tuple A " xL, L 0 , F , AP, Synch, Auty where L is a finite set of locations, 0 P L is the initial location, F P L is the

	final location, Synch Ď L ˆBAP ˆInC ˆ2Act ˆ H, Ó	( ˆBAP ˆL is the set of synchronizing
	transitions, and Aut Ď LˆB AP ˆBoundCˆ7ˆ H, Ó	( ˆL is the set of autonomous transitions.

  , uy, when i ď K, ÝÝÝÝÝÑ with ´‰ and all u, one creates transitions:

				´γ´^α i´1 ăxďαi,B ÝÝÝÝÝÝÝÝÝÝÝÝ Ñ x , iy and Ý ´γ´^α K ăx,B
	For all transition	´γ´, B ´,Ó	´γ´, B ´,Ó ÝÝÝÝÝÑ
	x , 0, uy and	´γ´, B ´,Ó ÝÝÝÝÝÑ x , 0y.
	For all synchronized transition	γ `,B `,r ÝÝÝÝÝÑ `with `‰ and all i, u, one creates transitions: Ý
	x , i, uy	γ `^xăcu ,B ´,r ÝÝÝÝÝÝÝÝÝÝ Ñ `and x , iy Ý	γ `,B ´,r ÝÝÝÝÝÑ Ý `.

Ý

ÝÝÝÝÝÝÝÝÑ x , K `1y.

  and x , iy

			γ `,B ´,Ó ÝÝÝÝÝÑ x , 0y.
	For all synchronized transition u	γ `,B `,r ÝÝÝÝÝÑ `with `‰ , one creates transitions: for all Ý
	i, x , i, uy	γ `^xěcu ,B `,r ÝÝÝÝÝÝÝÝÝÝ Ñ Ý `.

For all k define r 1 k by r 1 k " H if B k " 7 and r 1 k " r k otherwise. For all k define c k , d k by c 0 " d 0 " 0 and for k ą 0:

if

The integer c k represents the difference between the values of the clock in the k th states of the original and simulating runs while d k represents how c k has to be taken into account in the k th state of the simulating run. In general, d k is equal to c k except when the original run goes through a guard x ą C in which case the difference between the clock values is irrelevant.

The main point is that all transitions in ρ can be mimicked due to the choice of K.

n , δ n q ¨¨¨be a run of A 1 . For all k define r k as the original reset that associated with the creation of the transition labelled by γ k `dk´1 , A n , r 1 k . For all k define c k by c 0 " 0 and for k ą 0:

n ćn , δ n q ¨¨¨is a run of A.

đ § Proposition 15. There exists a family tA n u nPN in A rc such that the size of A n is Opn 2 q and for all A P A nar with LpAq " LpA n q, p|Aut| `1q|Synch| ě 2 n .

Proof. Consider the automaton A n described below. Here Act is a singleton and so we omit the labels of the actions.

Given a valuation v of the atomic propositions, let us define the integer zpvq P r0, 2 n r by: zpvq " ř iďn 2 i´1 1 vppiq"J . Observe that z is a one-to-one mapping. Then A n accepts the timed paths starting with some initial valuation v such that the first action occurs not earlier than zpvq. Assume by contradiction that there exists A P A nar with LpAq " LpA n q such that p|Aut| 1q|Synch| ă 2 n . Consider 2 n accepted timed paths σ v starting with the 2 n possible valuations v such that the first action occurs at time zpvq. Let t v " v γv,rv ÝÝÝÑ 1 v be the synchronized transition in A corresponding to this action and, xv be the clock valuation when entering v . Observe that this clock valuation is either 0 or a time constant occurring in an autonomous transition. Due to the assumption, there are two different valuations v and v 1 with t v " t v 1 and xv " xv 1 . W.l.o.g. let zpvq ă zpv 1 q. Consider a timed path starting with valuation v 1 and whose first action occurs at time zpvq. Such a path is accepted by A using the accepting


Pierre Saulais
email: pierre.saulais@telecom-em.eu

Inventive Intellectual Corpus Analysis Applied to Incremental Technological Innovation

Keywords: Stimulated creativity, Intellectual Corpus Analysis, Knowledge based innovation, KM analysis tool

Our concern deals with the Knowledge Based Innovation domain in an industrial context. When a creative idea is generated, its transformation into new knowledge depends on a cycle associating three subsystems and highlighting the link between idea and knowledge: the individual who generated the idea, the knowledge field which acts as a reference repository and the knowledge community who evaluates, selects and validates relevant ideas.

Usual innovation dynamic is based on creative problem solving (from problem to solution). This paper covers the reversibility of the link idea-knowledge, that is to say the passage from knowledge to inventive idea. We promote an ab nihilo innovation dynamic (from ideation to innovation). In this paper, we propose an inventive idea generation method which takes advantage of the inventive intellectual Corpus of Knowledge actors. The research is dedicated to the epistemic connection between the structural analysis of knowledge contained in inventive intellectual Corpus and the ideation seen as inventive knowledge generation.

Our methodology consists in building a theoretical representative model and in validating it through experimentation. Model's input data represent a cognitive stimulus and model's output data consist of a prospective vision. Cognitive stimulus is based on in-depth analysis of the texture of knowledge structuring the inventive intellectual Corpus.

Results include experimental validation of the Knowledge Based Innovation approach. Our contribution consists in showing that ideation, stimulated by the critical analysis of the structure of knowledge lying in the knowledge actor's inventive intellectual Corpus, can be seen as an epistemic mutation, where source, process, results, corpus and knowledge actor can be assimilated as an unique entity.

An illustration of possible software implementation is given, derived from existing KM extraction software suite.

Introduction

Firms' strategy is now based on innovation. The innovative activity highlights the ability of firms to maintain their competitive advantage. According to [START_REF] Drucker | Innovation and Entrepreneurship[END_REF], innovation consists in looking for change in a determined and organized manner and in systematically analyzing opportunities which such changes can bring in terms of economic and social progress [START_REF] Prax | Objectif : Innovation[END_REF]. We can see that the innovation concept sends us to multiple research fields belonging to firm strategy, to marketing or to project management [START_REF] Soparnot | Management de l'innovation[END_REF]. The word Innovation has several meanings, which can represent either the creative process able to generate a new element having an economic and social value, either the acceptance of this element by a community, either this element itself [START_REF] Fernez-Walch | Management de l'innovation[END_REF]. Our concern takes place in the new domain of Knowledge Based Innovation [START_REF] Amidon | Innovation et management des connaissances[END_REF]: we want to highlight the link between Knowledge and Ideation in the sense of creation, formalization and sequencing of inventive ideas according to an intellectual process that structures a conceptual seed in a reasoned way [START_REF] Saulais | Connaissance et ideation[END_REF]. We can see that the link between idea and knowledge comes from the very principle of validation. Our questioning

Pierre Saulais

regards the reversibility of the idea-knowledge link, that is to say the way from knowledge to inventive idea. Our research question can be expressed as follows: which epistemic connection can we make between the analysis of the structure of the knowledge included in the inventive intellectual Corpus and ideation in the sense of inventive Knowledge creation?

State of the Art and conceptual framework

Knowledge capital and inventive intellectual Corpus

According to a conventional approach of knowledge capital [START_REF] Ermine | La Gestion des connaissances[END_REF], there is confusion between capital and Corpus. Our own analysis consists in discriminating capital from Corpus [START_REF] Saulais | Application de la gestion des connaissances à la créativité des experts et à la planification de la R & T en milieu industriel de haute technologie[END_REF]. So, Ieaning on the Intellectual Property Code, we consider a capital as a group of assets able to generate revenue and an intangible capital as a group of intangible assets [START_REF] Saulais | Application de la gestion des connaissances à la créativité des experts et à la planification de la R & T en milieu industriel de haute technologie[END_REF]. An invention patent is made of an intellectual content, which, when meeting patenting requirements, gives a property act to its owner: intellectual content belongs to Corpus and property act belongs to capital [START_REF] Saulais | Application de la gestion des connaissances à la créativité des experts et à la planification de la R & T en milieu industriel de haute technologie[END_REF][START_REF] Saulais | L'idéation fondée sur l'analyse de la structure de la connaissance[END_REF]. With its dematerialized nature, Inventive intellectual Corpus is made of existing or recently acquired Knowledge specific to an individual and able to generate intellectual property rights [START_REF] Saulais | Application de la gestion des connaissances à la créativité des experts et à la planification de la R & T en milieu industriel de haute technologie[END_REF][START_REF] Saulais | Connaissance et ideation[END_REF].

State of the art of innovation process

In this section, we will focus on industrial state of the art then on academic state of the art of innovation process.

Industrial state of the art

In the industrial world in general, innovation process follows the « pipeline » model (Figure 1). This innovation model comes from the development model called « Development Funnel » [START_REF] Wheelwright | Revolutionizing Product Development: Quantum Leaps in Speed, Efficiency and Quality[END_REF]. In Figure 3, reflexivity context is given from outside towards engineering team. This kind of innovation dynamic works on a "heteronomic" mode (which extracts its rules from outside).

Figure 3: From problem towards solution

In Figure 4, reflexivity context is given from outside towards inside. This kind of innovation dynamic works on an "autonomic" mode (which gives rules for itself).

Figure 4: From ideation towards innovation

In both cases, innovation activities are leaned on ideas production, which are the essential resource. Classical creativity methods are matched to the first innovation dynamic which is problem-solving oriented. We can legitimately explore the innovation dynamic described in Figure 4, powered by new ideas generation issued from the analysis of existing intellectual Corpus.

Strategic Preparation

Parameters & targets definition

Problematic building

Ideas generation

Concept design & qualification

Concept selection Production Deployment & evaluation

Academic state of the art [START_REF] Fernez-Walch | Management de l'innovation[END_REF] suggest height different conceptual aspects for the innovation process: valorization of technical progress, acceptance of a new product, whirling process, marketing plan, political process, technical system transformation, learning process.

Innovation process management has multiple dimensions: [START_REF] Trott | Innovation Management and New Product Development[END_REF]) highlighted product innovation management, [START_REF] Van Stamm | The Innovation Wave[END_REF] and (Bruce & Bessants 2001) insisted on design. Several literature compilations cover this field, among which the best known is directed towards the United States [START_REF] Burgerman | Strategic Management of Technology and Innovation[END_REF]). [START_REF] Tidd | Management de l'innovation : Intégration du changement technologique, commercial et organisationnel[END_REF]) also show how firms are inevitably limited in their innovation strategies by their past and current abilities.

Furthermore, a Knowledge Management approach can be included in the innovation process management: Debra Amidon (2001) locates the innovation power in the intellectual Corpus, coming from the combination of a quick share of knowledge and of the new applications evolution applications.

Use of knowledge for the research of innovative solutions

Innovation process can usually be described in four steps (Louafa and Perret, 2008): question description, divergent ideas production, convergence of generated ideas towards the given question, selection and choice.

Current techniques for divergent ideas production aim at generating as many ideas as possible in a given restricted time by stimulating imagination. Creativity methods aim at modifying knowledge by adapting them, recombining them, giving them another sense and another value (Louafa and Perret, 2008).

Using knowledge to discover innovative solutions is already part of some industrial design methods:

 The TRIZ method (« Theory of Resolution of Inventive Problems ») is dedicated to the resolution of technical problems requiring innovative solutions [START_REF] Altshuller | Creativity as an Exact Science: The Theory of the Solution of Inventive Problems[END_REF] ;  The C-K (Concept-Knowledge) Theory: [START_REF] Hatchuel | C-K design theory: an advanced formulation[END_REF] developed the C-K Theory in design engineering in order to formalize a real approach of creative design. It's one of the present examples of an approach based on Knowledge.

In the present paper, considering that « inventive design » is not the vocation of the method we developed but only one of its effects, we proposed to develop a Chaotic-inspired evolution model for knowledge (section 4).

State of the art in terms of models

We borrow to Jean-Louis [START_REF] Ermine | La Gestion des connaissances[END_REF] the principle of the model basis (Figure 5 and Figure 6) described through steps 1 to 4. We wish to briefly recall how this basis is built. Building of the existing part of the model may be described as follows:

Step 1: Knowledge is part of a complex system

Aiming at conciliating connections between the all and the parts and at taking into account the complexity of the phenomenon under study, the Systems Theory progressively integrated every domain of knowledge, as Edgar Morin clearly shown (Morin 2008c).

Step 2: Knowledge creation is seen as an evolution of the knowledge system

In the Theory of Complexity, emergence characterizes the spontaneous apparition of a new structure in the considered medium, which cannot be explained by a simple combination of elements or of processes structuring the medium [START_REF] Heudin | L'évolution au bord du chaos[END_REF]. According to the Evolution Theory, Knowledge capital is not fixed but it follows a constant and fast evolution [START_REF] Ermine | La Gestion des connaissances[END_REF]. A very important assumption in the innovation domain comes from economics through the « path dependency » assumption [START_REF] David | Dépendance du sentier et économie de l'innovation : un rapide tour d'horizon[END_REF], for which innovation is an « endogenous and cumulative technological creation » mechanism. [START_REF] Ermine | La Gestion des connaissances[END_REF] proposed another method based on Knowledge (Figure 5), with two steps (analysis of Knowledge corpus and discovery of innovation well and innovation laws).

Figure 5: Innovative Knowledge creation process

Elaboration of evolution laws from knowledge drill (Figure 5) presents some analogy with innovation creation by recombination, either through knowledge brokerage [START_REF] Hargadon | Firms as Knowledge Brokers: Lessons in pursuing continuous innovation[END_REF][START_REF] Hargadon | Créer un laboratoire d'innovation[END_REF], elements association in innovations distribution in order to prepare a rupture [START_REF] Fleming | Breakthroughs and the 'Long Tail' of Innovation[END_REF], recombination of innovations [START_REF] Fleming | Recombinant Uncertainty in Technology Search[END_REF], combination of new knowledge and existing knowledge [START_REF] Nerkar | Old is Gold? The Value of Temporal Exploration in the Creation of New Knowledge[END_REF].

Step 3: Thanks to the path dependency assumption, we postulate that knowledge evolution seen as complex system can be described by another complex system

The path dependency hypothesis explains the strategic diversifications of the firms and it can also explain how innovations appear in organizations. Existing knowledge are conditioning future ideas leading to innovation, which fits [START_REF] Cohendet | La conception de la firme comme processeur de connaissances[END_REF] who consider the firm as a knowledge processor.

To sum up, the hypothesis made by Jean-Louis Ermine consists in the assimilation of the knowledge creation process to the firm knowledge capital evolution process, based on the creativity of the knowledge actors, inside the firm but in interaction with their environment.

Step 4: The evolution process can be generalized to any time-dependent complex system A general evolution model can be derived from the analysis of emergence in biological systems [START_REF] Heudin | L'évolution au bord du chaos[END_REF].

A system is built on structures which may vary when some energy is brought to the system. This transformation is regulated by the feedback which confronts these structures with their environment. The finality of these structures is expressed in terms of properties. When transformed, these structures get new properties. The evolution process only keeps the property compliant with the system's finality, thanks to the stabilization loop. Rejected properties represent the system entropy. This operation of relevant properties creation is an emergence phenomenon since it represents a new and matched solution for the evolution of the system under analysis (Figure 6).

An analogy can be highlighted between creativity process and a process called « chaotic » [START_REF] Gleick | Chaos[END_REF][START_REF] Prigogine | La fin des certitudes[END_REF], characteristic of a divergence process. However, introducing a regulation loop allows the emergence of a stable structure by filtering the outputs generated by divergence: it's the emergence phenomenon. This structure is a new and matched solution to the given problem and so does the creativity problem.

Innovative Proposals Evolution Laws Potential Innovation Well

Knowledge Corpus

Analysis

Ideas Generation

Innovation

Existing Knowledge Analysis

Innovative Design Ideas History Experiments

Knowledge Corpus

Figure 6: The general evolution model To sum up, according to [START_REF] Heudin | L'évolution au bord du chaos[END_REF], the evolution process can be generalized to any time-dependent complex system, thanks to four sub-processes: variation out of balance following energy supply, feedback, emergence and stabilization towards balance (Figure 6).

Methodology

Our methodology is based on experimental method, aiming at building a representative theoretical model (Figure 7) and at validating it by an experiment (section 5) using collected data.

According to [START_REF] Lalande | Vocabulaire technique et critique de la philosophie[END_REF], experimental method really consists of observation, classification, hypothesis and validation by appropriate experiences. In other words, experimental method consists in inferring some observable consequences from a law, an hypothesis or a theory and, most often thanks to an observation and measurement process, in determining if these consequences fit facts or not. For the theoretical model, input data are seen as a cognitive stimulus corresponding to the different temporal sections of the inventive Knowledge trajectories included in the inventive intellectual Corpus and output data are seen as a production materialized as a prospective vision. The experimentation instantiates the theoretical model thanks to individuals solicited as Knowledge actors (Figure 8).

Theoretical model

In previous section 2, we saw an initial model (Figure 6, steps 1 to 4 of section 2.4). Our contribution mainly includes step 5 (Figure 7) and step 6.

Step 5: The theory of Chaotic-inspired evolution by emergence can be applied to the creation of inventive knowledge

As we deal with a system facing evolution, we apply the general model of evolution to the creativity problem, thanks to already collected theoretical elements, in order to get the model of Chaotic-inspired model of inventive Knowledge by emergence (Figure 7). to keep the link with thermodynamics. Then the fact of emergence shows itself as apparition of new qualities which can't be reduced nor deduced from the properties of initial components.

So, the Knowledge creation process can be represented as an instable non-linear dynamic system, unpredictable for the long term and based on the Second Principle of thermodynamics [START_REF] Saulais | Créativité et gestion des connaissances[END_REF]. According to the Chaotic reasoning, creativity starts with a kind of tension between the desire of evolving towards an upper form of organization (negentropy) and a statement of evolution towards a lower form of organization (entropy). This tension can free itself only by a conceptual idea (creativity), structured by reasoning into an invention idea to be concretized in an innovative product [START_REF] Saulais | Application de la gestion des connaissances à la créativité des experts et à la planification de la R & T en milieu industriel de haute technologie[END_REF].

According to Figure 7 model, organized Knowledge will be improved thanks to the cognitive stimulus. We think that the model described in Figure 7 is relevant to set up an operating mechanism of idea generation regulated, weighted and oriented towards the firm objectives, on which our ICAROS ® method is based (See Step 6 below and section 5).

Step 6: Activation of Chaotic-inspired model of Knowledge evolution by emergence thanks to ICAROS ® method

The ICAROS ® (Intellectual Corpus Analysis for Reasoned Openmindness Stimulation) proposed stimulated creativity method aims at activating the Chaotic-inspired model of Knowledge evolution by emergence (Figure 7), from the creation of a cognitive stimulus: this cognitive stimulus is derived from the inventive Knowledge creation process illustrated in Figure 5 by limiting Knowledge Corpus to inventive intellectual Corpus: Knowledge actors represent experts organized in communities, carrying reference Knowledge both on external environment (markets, state of the art, …) and on internal environment (specific tangible and intangible resources of the firm). For our approach, we center our frame of reference on the Knowledge actor and not on the organization, as long as we focus on the upstream part of the creativity concept, which belongs to the individual [START_REF] Saulais | Application de la gestion des connaissances à la créativité des experts et à la planification de la R & T en milieu industriel de haute technologie[END_REF].

Our new use of inventive intellectual Corpus as dematerialized corpus directly comes from the mental scheme based on inventive Knowledge likely to generate intellectual property rights.

We note the attractive aspect of the representation of Knowledge creation as a result of a systemic evolution process, in the frame of order/disorder dialogic, of time irreversibility and of substitution of possibilities to certitudes: it's in probabilistic representations that creativity may find its place.

Thales case study

The objective of this section is to link the experimental procedure and the elements of the theoretical model.

Context

Stimulated creativity process uses current community, in the sense presented in the special issue of Management review (HEC-Montréal, 2010), organized in Knowledge & Technology Portfolio Domains.

Global presentation of stimulated creativity process

We now describe the creativity process as applied (Figure 8).

Phase 1: Preliminary: Intellectual Corpus inventory

Figure 9 describes the methodology of the preliminary phase, consisting in the inventory of inventive tracks related to one Knowledge domain, projected onto a Knowledge map, which is the input of the creativity stimulation process.

Figure 9: Preliminary Inventory

The firm develops and produces technical objects, presently surface radars. A technical object should not be seen through the organization / production processes prism, but as an autonomous a priori object which holds intrinsic Knowledge. This Knowledge must be described in a non-contextual language, available for many communities, even outside the organization. We decomposed the technical Radar object into ten technical domains. Each domain can be seen as a complex system [START_REF] Bertalanffy | General System theory: Foundations, Development, Applications[END_REF]), which is classically described according to systemic points of view: functional (what the systems does), structural (what the system is), teleological or applicative (what the system is designed for) and a genetic aspect (system evolution) represented by the time axis of the other points of view. Figure 8 gives an example of cognitive map for the algorithm domain. Independently from the ICAROS ® experiment on creativity stimulation, the inventory of inventive activity of more than sixty experts during the past three decades in the three main fields of the company and its reasoned synthesis leads to a large amount of strategic material that only very few companies search for resources to build. 7): Individual creativity stimulation Stimulated creativity individual sessions include the following steps: presentation to the expert of the tracks projected in the Knowledge map, analysis of the tracks by the expert and statement of his prospective vision for his domain. Each half-day long session was recorded.

Phase 2 (First loop of Figure

During stimulated creativity individual session, each expert is requested to react to the representation of inventive tracks of past years in his own Knowledge domain. They must then determine how their own analysis of the past and present situation described in terms of dated inventive tracks could logically be transformed into a prospective view of what future inventive Knowledge are to be created or acquired. This prospective formalization of their vision of their Knowledge domain leads to motivated proposals of study projects to be candidates as inputs to the innovation procedure.

After a detailed analysis of the session records, a synthesis of each session led to a prospective document validated by the expert. All prospective documents are synthetized into a complete structured vision giving numerous axes to technical transverse strategic activity.

Phase 3 (Loop 2 of Figure 7: Collective co-building of prospective vision

Creativity stimulation process is applied to the entity Knowledge actors through three steps (Figure 10). Initialization of this phase was performed by the redaction of the prospective document including all the proposals from each stimulated expert: the prospective elements provided by the creativity individual sessions were successively confronted to different groups, the technical peers, the technical field experts, the representatives of technical strategy and of the strategy of the organization.

The seminar report includes, for each domain the major R&T problems that determine the future stakes and the way to solve them.

Phase 4 (First loop of Figure 7): Diffusion of results

Phase 4 deals with the diffusion of results to dedicated actors as prospective vision shared be experts and by managers.

Results

Results include experimental validation of the Knowledge-Based Innovation approach:  Inventive intellectual Corpus includes elements able to represent inventive trajectories linking inventive intellectual tracks (patents, advances studies reports). Inventory of individual inventive intellectual Corpus on several ten decades projected in inventive Knowledge maps allows to determine, understand and explicit the inventive trajectories ;  A reasoned analysis of the tracks gives the intellectual progress along the tracks (acquisition of a method, in-depth analysis, questioning about variant, bifurcation and drop) ;  Creation of numerous prospective elements from an in-depth reflection based on the analysis of the numerous different time segments of inventive Knowledge trajectories points out the emergence of new material able to improve inventive intellectual Corpus ;  Creativity stimulation is firstly applied to Knowledge experts representing each their Knowledge domain.

Creativity stimulation is used to help knowledge experts determining and clarifying their individual prospective elements in order to help them building a prospective vision of their domain.

Our contribution consisted in showing that ideation, stimulated by the critical analysis of the structure of Knowledge lying in the Knowledge actor's inventive intellectual Corpus, can be seen as an epistemic mutation, where source, process, results, Corpus and Knowledge actor can be assimilated as an unique entity.

Illustration of possible software implementation of ICAROS

® method in IP Metrix™ TKM software suite IP Metrix™ KM extraction software suite was developed by TKM (TecKnowMetrix), a spin-off2 from Grenoble University Laboratory specialized in data mining applied to scientific and technological literature (analysis of heterogeneous corpus, data mining on huge quantities of data, automatic processing and normalization, parametric dashboards). This KM extraction software suite is dedicated to a simple firm environmental search or to an in-depth bibliographic analysis. Its heart is made of a very large Knowledge base (patents, scientific literature, technical literature, European projects, firm monographs) constantly updated and stored on a secured server.

Discussions are currently in progress between the two co-authors in order to include the ICAROS ® method in IP Metrix™ TKM software suite. Main idea is to implement some rise in Information Value Chain or DIKW chain (See Figure 1Figure 11). DIKW chain is composed of Data, Information, Knowledge and Wisdom, defined as follows:

 Data: simple signs without intention  Information: collection of organized data  Knowledge: Information-based representation representing realities of the world  Wisdom: ability to action structured Knowledge and comprehension in a reasoned way, in order to determine and reach creation objectives Considering the IP Metrix™ TKM software suite as a relevant information processor and the ICAROS ® method as a relevant ideation method for inventive activity, the co-authors' finality is to extend present capacities to achieve an implementation of a Knowledge base-supported software tool dedicated to inventive Knowledge generation (See Figure 12).

Results discussion

With respect to literature, this paper gives numerous contributions. On one hand, it illustrates an experimental validation of the Knowledge-Based Innovation (KBI) method as described in section 5.6. On the other hand, theoretical results can be described as follows:

 Ideation is stimulated by the critical analysis of knowledge included in knowledge actor's inventive intellectual Corpus ;  Ideation is seen as an epistemic mutation where source, process, results, Corpus and actor may be assimilated as a unique entity ;  A new link was established between intellectual property domain (inventive intellectual Corpus), Knowledge management domain (cognitive stimulation based on the analysis of the structure of the knowledge included in inventive intellectual Corpus) and innovation management domain (creation of inventive Knowledge).

With respect to management practice, contributions of present paper lay on the demonstration that the ICAROS ® method of ideation based on Knowledge is an alternative to open innovation, where the opening was made as a preliminary and where the approach through Knowledge highlights the fact that the prospective analysis in not applied on the product but on the structure of the Knowledge carried by the technical object considered as a Knowledge object. Furthermore, co-operation considered in a close future by the co-authors aims at improving management practice by achieving the implementation of a Knowledge base-supported software tool dedicated to inventive intellectual Corpus analysis and inventive Knowledge generation.

Data

Conclusion

We described a theoretical model of emergence-evolution Knowledge and a structured method, ICAROS®, based on the activation of this theoretical model of inventive Knowledge creation able to feed the innovation procedure. Our approach based on the dual concept of creation (creativity-inventivity) suggested that inventive Knowledge creators could be considered as the center of the method, after the prerequisite inventory of inventive activity and structuration of the inventive intellectual Corpus carried by the Knowledge actors.

In a financial context not favorable to internal R&D investments, in order to stimulate innovation, Knowledge-Based Innovation could be a very effective alternative to open innovation with its strong assumption of path dependency: it's the first degree of application of our method. The second degree of application of our ICAROS ® method, based on the creative determination of which creative knowledge are to be acquired, is made of an epistemic mutation which represents a very promising research axis for an in-depth exploration.

Co-operation considered in a close future by the co-authors aims at improving management practice by achieving the implementation of a Knowledge base-supported software tool dedicated to inventive intellectual Corpus analysis and inventive Knowledge generation.

Figure 1 :

 1 Figure 1: The pipeline model for innovation according to Gidel (2004) Instrumentation du management multiprojects, cited in (Fernez-Walch et Romon, 2006) A recent study conducted by the Club Gestion des Connaissances 1 proposed a synthesis of numerous innovation methods used in firms: it shows that all these methods approximately follow the same process (Figure 2):

Figure 2 :

 2 Figure 2: Innovation process In an industrial context, technical innovation activity schematically depends on two innovation dynamics:  Confrontation with a given technical problem requiring an innovative solving. It's a closed innovation process where the framework is the problem itself (Figure 3) ;  The idea which having found a market. It's an open innovation process (Figure 4).

Figure 7 :

 7 Figure 7: The Chaotic-inspired model of Knowledge evolution by emergenceEvolution can be modeled by a dynamic non-linear instable function, fitting the chaos approach by the second principle of thermodynamics: it's the reason why we called « Chaotic-inspired » the model (Figure7) in order

Figure 8 :

 8 Figure 8: Knowledge based creativity process

Figure 10 :

 10 Figure 10: Example of cognitive map for the Algorithm domain Preliminary work was dedicated to the inventory and to the analysis of the past inventive tracks. It was carried over by the author as completely and objectively as possible. Tracks were collected during sixty-two individual interviews, for three technical domains, for a total of ninety three hours. Individual inventories are merged topic by topic to get the global inventive tracks. Intellectual Corpus elements are the inventive dated tracks of the last thirty years (patents, articles and papers, study reports, internal memos and white papers, presentation slides, training material), projected onto knowledge map, analyzed and synthesized by the author.

Figure 11 :

 11 Figure 11: DIKW Value Chain

Figure 12 :

 12 Figure 12: Role of IT in the KBI loop

French industrial association for KM diffusion, founded by Jean-Louis Ermine in 1999

TKM was launched by four researchers in 2004 following a very simple statement: main strategic decisions linked with innovation are based on interviews of experts but without preliminary control of information. However, one of the features of innovation process is the availability of this information: many information sources do exist, among which are patents, scientific literature but also technical literature, collaborative projects, web and so on