Timed interfaces:

Recently, we have proposed a new interface theory for Timed Systems (TS). Syntactically, our interfaces are represented as Timed I/O Automata, i.e., automata whose discrete transitions are labeled by Input and Output modalities. However,contrary to most preceding frameworks based on this model, we view TIOAs as timed games between two players: Input and Output. As suggested by de Alfaro and Henzinger for the untimed case, this approach allows for an optimistic treatment of operations on and between interfaces.

Our theory is equipped with typical ingredients of a compositional design framework: a satisfaction relation (to decide whether a TS is an implementation of an interface), a consistency check (to decide whether the specification admits an implementation), a refinement (to compare specifications in terms of inclusion of sets of implementations).
Moreover, the model is also equipped with logical composition (to compute the intersection of sets of implementations), structural composition (to combine specifications) and its dual operator Quotient. Our framework also supports incremental design. To the best of our knowledge, our theory is the first specification theory for TS in which both logical and structural compositions can be computed within the same
framework.

Both Refinement, Satisfaction, and Consistency problems can be reduced to solving timed-game problems. As an example, deciding whether an interface is consistent is equivalent to checking for the existence of a strategy that avoids states of the specification that cannot be implemented in the concrete design.

Our theory is implemented in ECDAR www.cs.aau.dk/~adavid/ecdar/, the tool leveraging the game engine UPPAAL TIGA www.cs.aau.dk/~adavid/tiga/ with the model editor and the simulator of the UPPAAL model
checker www.uppaal.com.

Unfolding of timed Petri nets:

Stochastic interfaces:

In 1991, Johnsson and Larsen proposed a formalism, Interval Markov Chains, for specifying Markov Chains. Instead of having fixed probabilisties, the formalism uses intervals of probabilisties on transitions:

We have investigated the complexity problems for this formalism such as deciding thorough refinement, common implementation, and consistency. The results are presented in the paper 'Decision Problems for Interval Markov Chains'.

Investigating this formalism shows that it is not closed under conjunction and parallel composition, and this has lead us to developing a more expressive extension aiding this problem, namely Constraint Markov Chains, that allow for general constraints:

The formalism, presented in the paper 'Compositional Design Methodology with Constraint Markov Chains' is equipped with notions of satisfaction, refinement, conjunction, parallel composition etc. 

The most recent contribution is the work on a specification theory for probabilistic automata, which is presented in the paper 'Abstract Probabilistic Automata'. This paper presents an extension of CMCs, that adds actions and modalities to transitions:

 The notions of satisfation, refinement, conjunction etc. uses the theory for Constraint Markov Chains together with the definition of modal refinement etc. from the theory of Modal Transition Systems.