{'fraction_non_alphanumeric': 0.04913713608220261, 'fraction_numerical': 0.013008826241601898, 'mean_word_length': 4.0032954358213875, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 20, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Modal Specifications for Probabilistic Timed Systems

Modal automata are a classic formal model for component-based systems that comes equipped with a rich specification theory supporting abstraction, refinement and compositional reasoning. In recent years, quantitative variants of modal automata were introduced for specifying and reasoning about component-based designs for embedded and mobile systems. These respectively generalize modal specification theories for timed and probabilistic systems. In this paper, we define a modal specification language for combined probabilistic timed systems, called abstract probabilistic timed automata, which generalizes existing formalisms. We introduce appropriate syntactic and semantic refinement notions and discuss consistency of our specification language, also with respect to time-divergence. We identify a subclass of our models for which we define the fundamental operations for abstraction, conjunction and parallel composition, and show several compositionality results.


Introduction
The design of complex embedded systems can be supported by component-based design methodologies, which can take the form of specification theories that provide the notions of abstraction and refinement, as well as a rich collection of compositional operators. A classical and widely used specification theory for component-based design is that of modal automata [16]. A modal automaton is essentially a deterministic automaton equipped with may-and must-transitions, which are respectively used to specify allowed and required behavior. Several technical aspects of modal automata have been studied in the literature, including modal vs. thorough refinement, consistency, abstraction, as well as operators for parallel composition of components and conjunction, where the latter supports independent development. These notions enjoy a number of important properties, e.g., that conjunction is the greatest lower bound w.r.t. modal refinement and that abstraction is compositional. In this way, modal automata provide mathematical foundations for designing and reasoning about component-based systems at the abstract level of interfaces and to derive properties on the implementation level of the global system.
In recent years, much attention has been dedicated to formulating quantitative extensions of modal automata, for example to support the development of component-based systems which feature real-time and/or probabilistic behavior. An example of these developments are a modal specification language for timed systems called Modal Event-Clock Specifications (MECS) [4]. MECS are essentially a modal extension of Event-Clock Automata (ECAs) [2], which form a strict subclass of the classical Timed Automata [1] model. Restricting to this model allows Bertrand et al. in [4] to lift a number of compositionality properties known for modal automata to the timed setting, i.e., to the model of MECS. Another recent quantitative variant are Abstract Probabilistic Automata [11] (APAs). While MECS are used to specify timed behavior, APAs enable the specification of abstract probabilistic behavior using probability constraints. Probabilistic behavior is commonly required for quantifying the likelihood of events, such as message loss in unreliable channels, or is exploited in the design of randomized protocols. Similarly to MECS, APAs are equipped with notions for conjunction and parallel composition, as well as a number of compositionality results that can be used for compositional reasoning and abstraction. However, in Structure. In Section 2, we recall relevant notions for APAs and PTAs. Section 3 introduces our new model of Abstract Probabilistic Timed Automata. In Section 4, refinement notions for APTAs are defined and compared. Section 5 is devoted to abstraction for APTAs. In Section 6, we define conjunction and parallel composition, and present compositionality results for APECAs (a strict subclass of APTA). Section 7 concludes and discusses future work.

Preliminaries
In this section, we recall important definitions for PTAs [14] and refer the reader to [11] and [13] for APAs. We first recall some elementary notions. A discrete probability distribution over a denumerable set S is a function µ : S → [0, 1] with s∈S µ(s) = 1. The set of all discrete probability distributions over S is denoted by Dist(S ). For a given s ∈ S , the point distribution µ s is the unique distribution on S with µ s (s) = 1. We denote by R + the set of non-negative reals. Let B 2 = {⊥, ⊤} and B 3 = {⊥, ?, ⊤} be the complete lattices with the respective orderings ⊥ < ⊤ and ⊥ < ? < ⊤, and meet (⊓) and join (⊔) operators.

Probabilistic Timed Automata
We now recall the standard timed automata notions of clock valuations and guards. For a finite set X of clocks, a clock valuation is a function v : X → R + . The set of all clock valuations over X is denoted by R X + . For any v ∈ R X + and t ∈ R + , we use v + t to denote the clock valuation defined as (v + t)(x) = v(x) + t for all x ∈ X. We use v[Y := 0] to denote the clock valuation obtained from v by resetting all of the clocks in Y ⊆ X to 0, and leaving the values of all other clocks unchanged; formally, v[Y : We write 0 for the clock valuation that assign 0 to all clocks.
Let X = {x 1 , . . . , x n } be a set of clocks. A clock constraint or guard g on X is an expression of the form x ∼ c such that x, y ∈ X, c ∈ R + and ∼ ∈ {≤, <, >, ≥}, or a conjunction of guards. A clock valuation v satisfies g, written as v ⊲ g, iff g evaluates to true when all clocks x ∈ X are substituted with their clock value v(x). Let CC(X) denote the set of all guards over X, and let CC N (X) denote the set of guards on X involving expressions with constants less or equal to N, where N is the maximal constant in all guards.
Definition 1 [PTA [14]] A probabilistic timed automaton is a tuple M = (L, A, X, AP, V, T, l 0 ) where L is a finite set of locations with initial location l 0 ∈ L; A is a finite set of actions; X is a finite set of clocks; AP is a finite set of atomic propositions; V : L → 2 AP assigns atomic propositions to locations; and T : L × CC(X) × A × Dist(2 X × L) → B 2 is a probabilistic edge function.
We write l g,a − − → µ iff T (l, g, a, µ) = ⊤, which comprises a source location l, a guard g, and a probability distribution µ which assigns probabilities to pairs of the form (Y, l ′ ), where Y ⊆ X is a set of clocks to be reset and l ′ is a target location. The behavior of a PTA is as follows: in any location a probabilistic edge can be taken if its guard is satisfied by the current values of the clocks. Once a probabilistic edge is nondeterministically selected, the choice for a particular target location and set of clocks to be reset is made probabilistically using µ.
We define the semantics of a PTA M by mapping it to a probabilistic automaton M by employing the classical region equivalence for timed automata [1]. A probabilistic automaton (PA) [17,11] M = (S , A, AP, V, T, s 0 ) consists of a set of states S with initial state s 0 , a set of actions A, a set of atomic propositions AP, a valuation function V : S → 2 AP and a probabilistic transition function T : S × A × Dist(S ) → B 2 . A region θ is the set of clock valuations which satisfy exactly the same guards of CC N (X).
Given a region θ, we write Succ(θ) for the union of all regions that can be obtained from θ by letting time elapse. Given a guard g ∈ CC(X), we write θ ⊆ g iff for all valuations v ∈ θ it holds that v ⊲ g. We denote the set of all regions by Θ N (X) and simply write Θ if clear from context. We now define the semantics of a PTA in terms of a PA. Definition 2 [Region PA] For a given PTA M = (L, A, X, AP, V, T, l 0 ), the associated region PA is given by , and T ′ is induced by T in the following way: for any l ∈ L and any θ ∈ Θ such that (l, θ) is reachable from (l 0 , 0), if l g,a − − → M µ then for each region θ ′′ ∈ Succ(θ) ∩ g there exists ζ : S → 2 X and µ ′ ∈ Dist(S ) such that In the derived region PA, the transition labels (θ ′′ , a, ζ) ∈ A ′ consist of the region θ ′′ that represents the time window in which the transition is taken, the fired action a ∈ A, and for each target state s ∈ S the set of clocks ζ(s) ⊆ X that are being reset when s is probabilistically chosen. W.l.o.g., we assume that R(M) is always pruned, i.e., all its states are reachable.
Similarly as shown for timed specifications in [4], any PA that is defined over the alphabet Θ × A × (2 X ) S can be interpreted as a PTA again. Intuitively, the states of the PA are interpreted as the locations of the corresponding PTA and the information about the guards, actions and clock resets for edges is derived from the transition labels of the PA. We introduce the operator T which translates any given PA M over the alphabet Θ × A × (2 X ) S into the PTA T (M). The application of T • R allows us, moreover, to define a normal form for PTAs.

Abstract Probabilistic Timed Automata
We now define Abstract Probabilistic Timed Automata (APTAs) as the central model of this paper. AP-TAs extend PTAs in three ways: (1) probability distributions are generalized to probability constraints, (2) may-and must-transitions are distinguished, and (3) locations are labeled with sets of admissible atomic propositions. All three modeling concepts are borrowed from APAs [11]. We use satisfaction relations to relate APTAs with PTAs that implement them. Let a probability constraint ϕ be a symbolic representation of a set of probability distributions over a set S . As in [11], we do not fix the language for probability constraints. The set of probability distributions that satisfy ϕ is denoted by Sat(ϕ) ⊆ Dist(S ). We define the constraints true and false, for which we require Sat(true) = Dist(S ) and Sat(false)= ∅. The set of probability constraints over S is denoted by PC(S ).

Definition 4 [APTA]
An abstract probabilistic timed automaton is a tuple A = (L, A, X, AP, V, T, l 0 ), where L, A, X, AP, l 0 are defined as for PTAs; V : L → 2 2 AP assigns sets of admissible atomic propositions to locations; and T : L×CC(X)×A×PC(2 X ×L)→B 3 is a three-valued probabilistic edge function. We use the notation l g,a ϕ to denote may-edges (formally if T (l, g, a, ϕ) = ?), l g,a − − → ϕ for must-edges (if T (l, g, a, ϕ) = ⊤), and l g,a ϕ for may-or must-edges, where g ∈ CC(X) is a guard, a ∈ A is an action, and ϕ ∈ PC(2 X × L) is a probability constraint. Fig. 1 depicts an example APTA modeling a scheduler component. In the initial location l 0 , tasks can be submitted to the scheduler and will be started within 1 time unit. Two types of tasks can occur: short-and long-running ones. The choice between them is probabilistic according to the probability constraint ϕ p = (0.25 ≤ p 1 ≤ 0.75) ∧ (0.25 ≤ p 2 ≤ 0.75) ∧ (p 1 + p 2 = 1). Tasks either finish in the expected time frame or can be canceled at any point. The canceling of tasks is modeled using may-edges, and thus is not required to be realized by implementations. {{idle}} Figure 1: An example APTA specification for a scheduler component.

Example 1
We say that M satisfies A, denoted M | = A, iff there exists a satisfaction relation relating l 0 and l ′ 0 . If M | = A, M is called an implementation of A.
Condition 1 states that any must-edge in the specification is required to be realized in an implementation (possibly split up into several edges emitting from one location). Condition 2 ensures that any edge in the implementation is allowed by the specification (as a may-or a must-edge). Note that, since M is in normal form, the guard in the edge l g,a − − → M µ is necessarily a region. The set of all implementations of A is given by A = {M | M | = A}. Example 2 Fig. 2 depicts an implementation of the APTA for a scheduler component in Fig. 1. We indicate the satisfaction relation by using equal location indices, e.g., the locations l 3 and l ′ 3 in the implementation are in relation with l 3 in the specification. The implementation differs from the specification in the following aspects. After a task has been submitted, the scheduler becomes busy, i.e., the set of atomic propositions {busy} is chosen for location l 1 . Two types of long-running tasks are distinguished in the implementation: ones that finish in the interval (2,6] and ones that finish in the interval (6,10]. Only tasks of the latter type can be canceled. The probability constraint ϕ p is realized by the probability distribution assigning 0.4 to l 2 , and 0.3 to l 3 and l ′ 3 , respectively. Note, however, that this PTA is not in normal form, because the location l 0 can be reached within three different regions: (0, 2], (2, 6] and (6,10]. Thus, by splitting up location l 0 , the normal form can be obtained and the satisfaction relation is constructed.

The Region-Based Interpretation
We show now that the check for the existence of a satisfaction relation between a PTA and an APTA can be reduced to a check for a satisfaction relation between their corresponding probabilistic region automata. Analogously to the mapping of a PTA to a PA using the region construction (cf. Def. 2), we can transform any APTA A into an APA R(A). In the resulting APA R(A), the types of the three-valued edge function are inherited from A. The transition relation and analogously for all may-edges.

Proposition 1 Consider an APTA
This proposition will be used later in Section 3.2.

Theorem 1 Given a PTA
A is called deterministic iff it is action-deterministic and AP-deterministic.
Note that Def. 6 is inspired by [11]. Action-determinacy can also be enforced on the syntactical level. However, such a definition would only be a sufficient, but not a necessary condition.

Consistency
Consistency of a specification refers to the property that there exists at least one model for this specification. In our setting, an APTA A is said to be consistent if it admits at least one implementation, hence formally iff A ∅. For any given APTA A, we can decide whether the APA R(A) is consistent and, if so, derive a PA M, such that M | = R(A) [11]. T (M) is then a PTA with finitely many states, and, by Proposition 1, a model of A.
In order to deal with consistency also on the syntactic level, we further define a location l ∈ L A in an ∅ and for all guards g ∈ CC(X), actions a ∈ A and probability constraints ϕ ∈ PC(2 X × L A ) it holds: if T A (l, g, a, ϕ) = ⊤ then Sat(ϕ) ∅. Note that inconsistency of a location does not imply inconsistency of the whole APTA. In order to decide whether an APTA is consistent, we follow the usual approach and use a pruning operator β that filters out distributions leading to inconsistent locations [11]. The detailed definition and properties of a pruning operator can be found in [13].
The following theorem shows that the application of β operator does not change the set of implementation. And it also implies that if β * (A) is empty, then A is inconsistent.
The above definition of consistency, however, places no restrictions on the derived implementations. In particular, the derived PTA could show unrealistic behaviors by preventing time from diverging. Therefore, we also aim at checking consistency in such a way that only divergent implementations are considered. Note that a divergent consistent APTA must be consistent, therefore we assume that the APTAs that we deal with are already consistent.
We consider the set of strict and probabilistic divergent (Sd and Pd, for short) implementations of A given by A Sd = {M | M | = A and M is strict divergent} and A Pd = {M | M | = A and M is probabilistic divergent}, respectively. The formal definitions of probabilistic and strict divergency can be found in [19] and [13]. Now we define an APTA to be Sd-or Pd-consistent if it admits at least one Sd or Pd implementation, i.e., A Sd ∅ or A Pd ∅.
Theorem 3 shows that a time-divergence sensitive consistency check for APTAs can be defined based on a reduction to APAs and stochastic two-player games. The details of this technique can be found in [13]. This result effectively allows us to check whether an APTA has at least one strict or probabilistic divergent implementation.

Theorem 3
An APTA A is Pd (resp. Sd) consistent if and only if in the game G(A), the -player has a winning strategy for the objective P =1 ( tick) (resp. objective tick).

Abstract Probabilistic Event-Clock Automata
We now introduce Abstract Probabilistic Event-Clock Automata (APECAs), which form a strict subclass of APTA, where clock resets are not arbitrary: each action a is associated with a clock x a which is reset exactly when the action a occurs. This kind of clock resets originated from Event-Clock Automata (ECAs) [2]: they form a strict subclass of TA, but they enjoy nice properties, e.g., they are closed under union and intersection, and can be determinized. • X A is a set of clocks where every x a ∈ X A corresponds to an action a ∈ A; Fig. 3 depicts two APECAs Cl and Acc. Cl models a clients requesting access to a given resource. It can either invoke get to request the resource; or grant to access it. The action extra is used when a privileged access with extended time is needed. We use ! and ? to indicate whether an action comes from the designed component or from its environment. The clock corresponding to the action get is x get . The client sends a second get-request at most one time unit after the first request. With a probability satisfying constraint ϕ 1 , the client terminates and stops requesting resources (state 2). The client can also request extended time at any moment while it is still active. Let the probability from state 1 to state 0 be p 1 and from state 1 to state 2 be p 2 in Cl. Then ϕ 1 could be defined as 0 ≤ p 1 ≤ 1/3 and p 1 + p 2 = 1. The APECA Acc specifies the behavior of an access controller. If the access to the resource is granted, then it should happen within 2 time units after reception of a get request. In case of a privileged access with extra time, this duration will be extended to at most 4 time units. However, with a certain probability (satisfying ϕ 2 ), the access controller will switch back to the default access time of 2 time units. The probability constraint ϕ 2 can be defined in a similar way as ϕ 1 . The use of probability constraints is explained in more detail in Examples 5 and 6.  Figure 3: The two APECAs Cl and Acc. The main difference to APTAs is that the probability constraints in APECAs are defined on L instead on 2 X A × L, and that we require completeness for the edge function. However, completeness is not a restriction, e.g., we model the case where in location l there exists no outgoing a-edge by setting T (l, true, a, false) = ?. Completing an APECA in this way does not modify its set of implementations. Note that a similar approach is also used in [4] to obtain completeness for timed modal specifications. An implementation of an APECA is a Probabilistic Event-Clock Automaton (PECA), which is a probabilistic variant of ECAs. PECAs form a strict subclass of PTAs. Formally, a PECA is a tuple C = (L, A, X A , AP, V, T, l 0 ), where L, A, AP, V and l 0 are as in PTAs, X A is as in the APECA, and T : L × CC(X A ) × A × Dist(L) → B 2 is a two-valued probabilistic edge function.
We write A 1 W A 2 iff there exists a weak refinement relation relating s 0 1 and s 0 2 .
Note that the correspondence function (see [13]) is not fixed in advance in weak refinements. This is the case in strong APA refinements [11], which we denote by S . We are now in a position to define our refinement notions for APTAs. While thorough refinement is a semantical inclusion between sets of implementations, strong and weak refinements are its syntactical counterparts. For the latter two, we apply the refinement notions for APAs to the induced region automata. A 1 = (L 1 , A, X, AP, V 1 , T 1 , l 0 1 ) and A 2 = (L 2 , A, X, AP, V 2 , T 2 , l 0 2 ) be two APTAs. We say that

Definition 9 [APTA refinements] Let
By Theorem 1, we can directly obtain that, for any APTAs A 1 and A 2 , it also holds that: where R(A 1 ) T R(A 2 ) refers to thorough refinement for APAs, which is also defined as inclusion of implementation sets [11] (analogously for Sd T and Pd T ). An example of a strong refinement can be found in [13]. The following theorem establishes a hierarchy among the different notions of refinement. We use RF 1 ⊃ RF 2 to indicate that the refinement RF 1 is strictly finer than the refinement RF 2 .
Theorem 4 APTA refinements form the following hierarchy: Sd T ⊃ Pd T ⊃ T ⊃ W ⊃ S . In Proposition 2, we relate weak and strong refinement with probabilistic time-abstracting bisimulation [7] for PTAs. In Proposition 3 we further show that strong, weak and thorough refinements coincide for deterministic APTAs. Proposition 2 Let ∼ denote probabilistic time-abstracting bisimilarity [7] on PTAs. If A 1 and A 2 are implementations, then (a) Proposition 3 For deterministic APTAs, where the sets of admissible atomic propositions in the initial locations are singletons, thorough, strong and weak refinement coincide. Fig. 5 also show that the Sdand Pd-thorough refinements do not coincide with each other or with thorough refinement even for deterministic APTAs.

Abstraction
The goal of abstraction is to hide internal details of a specification and thereby to obtain a simpler and usually smaller specification. In the setting of automata, an abstraction can be defined by partitioning the state space, i.e., by forming disjoint groups of states (or locations) where each of these groups is mapped to one abstract state (or location). Given a set of locations L, an abstraction function for L is a surjective function α : L →L. Its inverse γ :L → 2 L is called a concretization function. The abstraction of µ ∈ Dist(2 X × L), denoted α(µ) ∈ Dist(2 X ×L) is uniquely defined by α(µ)(l) = µ(γ(l)), for alll ∈L. Abstraction is lifted to sets of states, sets of distributions, and sets of probability constraints in a pointwise manner. It follows thatφ = α(ϕ) iff Sat(φ) = α(Sat(ϕ)). The abstraction of the product of constraint function ϕ and ϕ ′ is given as α(ϕ · ϕ ′ ) = α(ϕ) · α(ϕ ′ ).
A technical challenge in defining abstraction for APTAs is the handling of guards. For this purpose, we introduce a pre-processing step that syntactically transforms an APTA into an equivalent APTA such that an abstraction function can be applied.
Here, g calculates the common guards of all must-transitions emitting froml with action a. Given the function g, we define a pre-processing step for APTAs that splits some of the must-transitions such that abstraction has the intended meaning.
Given a guard g ∈ CC(X), we define the negation of g, denotedḡ ⊆ CC(X), as the set of guards, such that for any valuation v ∈ R X it holds that v ⊲ g if and only if there exists no g ′ ∈ḡ such that v ⊲ g ′ . The negation of a guard can be effectively computed by splitting the guard into its atomic comparisons and inverting the comparisons.
As a result of the pre-processing function, the guards on a must-transition are either the common guard determined by g, or are disjoint with the common guard. Since g(α(l), a) and g ∧ g ′ for all g ′ ∈ḡ(α(l i ), a) form a partition of g, it is easy to see that R(A) = R(P α (A)). We are now in a position to define the abstraction.

Proposition 4 For any APTA
A and abstraction function α, A W α(P α (A)).

Lemma 1 states that an abstraction function for an APTA A induces an abstraction function on R(A).
Proposition 4 follows directly from Lemma 1 and a similar result known for APAs [11]. This result is important in order to ensure that applying an abstraction yields a generalized specification, i.e., formally that the original specification always weakly refines its abstraction. Note also that we show in Section 6 that abstraction interacts well with parallel composition.

Example 4
Another client specification Cl 1 is depicted in Fig. 6(a), where state 1 in Cl is split into 1' and 1" in Cl 1 . State 1' can be seen as a "quick phase", since a get request should be sent in less than 2 time units, while state 1" is the "slow phase" due to the guard x get ≥ 2. Furthermore, in state 0' and 1', an extended time slot will be granted whether needed or not. However, in state 0', the additional time will only be granted after 1 time unit. From state 1", it is possible to either start from 0' again (quick phase), to move to state 1' (slow phase), or to state 2' (termination) after the access to the resource has been granted.

Conjunction and Parallel Composition
In this section, we define two composition operators for APECAs, i.e., conjunction and parallel composition. These two operators are intentionally defined only for APECAs, and not for general APTAs, in order to be able to ensure compositionality properties. Conjunction and parallel composition form the cornerstones for a specification theory supporting independent development and structural composition.

Conjunction
Given two APECAs E 1 and E 1 , their conjunction (or logical composition), denoted as E 1 ∧ E 2 , is the specification that realizes the conjunctive behavior of E 1 and E 2 . Specifically, the set of implementations of the conjunction approximates the intersection of the sets of implementations of E 1 and E 2 . We define conjunction here only for action-deterministic APECAs over the same set of actions. For two automata with different action sets, we add the missing actions in the respective automaton, and complete the edge function as explained in Section 3.3. We leave the generalization to nondeterministic APECAs for future work.

Definition 13 [APECA Conjunction
] Let E 1 = (L 1 , A, X A , AP, V 1 , T 1 , l 1 0 ) and E 2 = (L 2 , A, X A , AP, V 2 , T 2 , l 2 0 ) be two action-deterministic APECAs over the same sets of actions and atomic propositions. Their conjunction is for all l 1 ∈ L 1 , l 2 ∈ L 2 and T ∧ is defined as follows: for all a ∈ A, g 1 , g 2 ∈ CC(X A ), and l 1 ∈ L 1 , l 2 ∈ L 2 : 1. ∀ϕ 1 ∈ PC(L 1 ), ∀ϕ 2 ∈ PC(L 2 ) such that T 1 (l 1 , g 1 , a, ϕ 1 ) ⊥ and T 2 (l 2 , g 2 , a, ϕ 2 ) ⊥, let T ∧ ( l 1 , l 2 , 2. For all other ϕ ′ ∧ ∈ PC(L 1 × L 2 ) and g ′ ∈ CC(X A ) we define T ∧ ( l 1 , l 2 , g ′ , a, ϕ ′ ∧ ) = ⊥. Informally, the conjunction E 1 ∧ E 2 can be regarded as the largest specification that refines E 1 and E 2 . Note that we rely on the completeness of the edge functions. For example, assume that in l 1 there is a must-edge via the action a, and in l 2 the action a is not enabled. As we require completeness, the latter means that there is an edge l 2 g,a false. In the conjunction, this edge is combined with the must-edge from l 1 using Rule 1. Thus, in the conjunction we obtain the edge l 1 , l 2 g,a − − → false, which means that l 1 , l 2 is inconsistent. On the other hand, for may-edges no inconsistencies are produced.  Figure 7: APECA conjunction. Fig. 7(a) depicts Cl 2 as another version of the client. The conjunction of Cl and Cl 2 is shown in Fig. 7(b). Let ϕ 1 be defined as in Example 3 and let the probability from state 1" to state 0' be q 1 and from state 1" to state 1' be q 2 and from state 1" to 2' be q 3 in Cl 2 . We set ϕ 4 such that 0 ≤ q 1 ≤ 1/5, 1/3 ≤ q 2 ≤ 1 and q 1 + q 2 + q 3 = 1. Now let µ ∧ be any distribution satisfying ϕ ∧ . Let 6 . Those r's should satisfy the following constraints, given the constraints on the p's and the q's: r 1 + r 2 + r 3 = p 1 r 4 + r 5 + r 6 = p 2 r 1 + r 4 = q 1 r 2 + r 5 = q 2 r 3 + r 6 = q 3 .

Example 5
We use the notation A 1 ≡ A 2 to denote that both A 1 W A 2 and A 2 W A 1 . Next, we show that conjunction is preserved by the region construction.

Lemma 2 For any APECAs
We now show that conjunction is the greatest lower bound of APECAs w.r.t. weak refinement, after pruning the conjunction. Note that β * (E) means applying the pruning operator β on E for finitely many times. Theorem 6 relates the sets of implementations of the conjunction with the implementation sets of its components.

Parallel Composition
We now define a parallel composition operator for APECAs which enables modular specifications of systems. The formal definition is similar to the one for conjunction and requires again that all actions are shared. To enable interleaving of non-shared actions, we realize completeness of the edges differently. Let a be an action of E 1 that does not occur in E 2 . We now add a to the set of actions of E 2 and for every location l in E 2 we add a self-loop must-edge such that T 2 (l, true, a, ϕ) with Sat(ϕ) = {µ l }, where µ l is the point distribution on l. This is repeated for all non-shared actions of E 2 (symmetrically for E 1 ) until E 1 and E 2 have the same set of actions. This simplifies the definition of the parallel composition (and our proofs for related theorems) since interleaved and synchronized behavior can be uniformly treated using a single composition rule.

Example 6
Similarly to conjunction, parallel composition is preserved by the region construction (Lemma 3). Moreover, parallel composition interacts well with refinement (Theorem 7) and abstraction (Theorem 8). The latter result allows us to avoid state space explosion by applying abstraction component-wise instead of computing the complete system specification and then applying the abstraction. By Theorem 7 we also know that ≡ is a congruence w.r.t. parallel composition.

Conclusions
We introduced a modal specification theory of abstract probabilistic timed automata (APTAs) that capture systems which contain nondeterminism, probability and time. The theory supports refinement, abstraction, and the operations of parallel composition and conjunction, the latter for independent development. The main challenge in combining probabilistic and timed behaviour was due to the need to consider guards of transitions, as well as a time-divergence sensitive consistency check. In order to obtain a compositional theory, we had to restrict to the class of abstract probabilistic event clock automata (APECAs).
As future work, we aim at finding a class of modal specifications for probabilistic timed systems that, in terms of expressiveness, lies between APECAs and APTAs, but still enjoys the compositionality properties of APECAs. Moreover, we plan to extend our work on abstraction to support counterexample generation.