Project topics and materials
Get Complete Project Material File(s) Now! »
A coalgebraic definition of systems
We first introduce another way to define systems via coalgebras. This definition is just the expression using coalgebraic formalism & notations of our functional definition of systems introduced in Chapter 3. We will use it to define a logic on coalgebraic systems.
Preliminaries
We will use many terms and notations from the coalgebraic theory. To help the intuition, we recall in this subsection some coalgebraic notions that will be used in this chapter. A coalgebra can be seen as an abstraction of transition systems (i.e. automatas) of all kinds. A coalgebra consists of a set S equipped with a transition function : S → F(S) where F : Set → Set is an endofunctor on the category Set of sets, defining the signature of the co-algebra . Hence, provides the set of states S with some structures. Unlike algebraic operations that enable to recursively build complex objects from basic objects given by signatures, coalgebraic operations are means to observe system states. More formally, we have:
Definition 5.1.1 (Coalgebra) Let F : Set → Set be an endofunctor, called signature functor. A coalgebra for F or F-coalgebra, is any pair (S, ) where:
• S is a set, elements of which are called states,
• : S → F(S) is a mapping, called transition mapping.
Coalgebras are well-adapted to define infinite data structures such as streams and infinite lists over an alphabet A, as well as all kinds of automatas. Hence, coalgebras for the signature functors A : S A S and A + 1 : S A S + 1 are respectively streams and infinite lists over an alphabet A, whilst coalgebras for the signature functors O I : S O SI, (O )I :S (O S)I and (2 )I : S (2S )I are respectively Moore, Mealy and nondeterministic automatas.
Definition 5.1.2 (Coalgebra morphism) Let (S, ) and (S′, ′) be two coal-gebras over a same signature functor F. A coalgebra morphism is a mapping f : S → S′ such that the following diagram commutes:
S f S′ α α′ F(S) F(S′) F (f ) Given a signature functor F, F-coalgebras and coalgebra morphisms clearly form a category noted CoAlg(F). An important notion in the categorical theory of coalgebras is the characteriza-tion of the final coalgebra that contains all systems behaviors (i.e. traces). Definition 5.1.3 (Final coalgebra) A final F-coalgebra ( , ) is a F-coal-gebra such that for every F-coalgebra (S, ) there is a unique coalgebra morphism !α : (S, ) → ( , ), that is: S →!α α π F(S) → F( ) F (!α) A final coalgebra, when it exits2, is unique up to isomorphism. A final coalgebra can be seen as a maximal representation of a system, that is which contains all system behaviors.
Transfer functions via coalgebras
Given a timescale, let us define the mapping T : T → T that from d ∈ T yields the latest d′ ∈ T such that d d′. Hence, dT is defined by: d if d ∈ T T otherwise pred (d) The following definition means that dataflows can be observed at any instant of time although their values only change at instants in their time scale.
Definition 5.1.4 (Snapshots) Let T be a time reference and T T be a time scale. Let f be a T-dataflow over A and let d ∈ T be an instant. The snapshot of f at time d, denoted f :: d, is the element f (dT) of A. Similarly to Rutten’s work in [56], we will show that the behavior of systems can be characterized by causal functions mapping infinite inputs to infinite outputs sequences. Hence, observable behaviors of systems are given by causal transfer functions (equivalent to the transfer functions defined in Chapter 3):
Definition 5.1.5 (Transfer function) Let In and Out be two datasets denot-ing, respectively, the values in input and in output. Let T be a time reference. Let T T be a time scale. A function F : InT → OutT is a transfer function if, and only if it is causal, that is: ∀d ∈ T, ∀f, g ∈ InT , (∀d′ d ∈ T, f :: d′ = g :: d′) ⇒ F(f ) :: d = F(g) :: d Then, let us define the mapping T : T → T that from d ∈ T yields the least d′ ∈ T such that d′ d. Hence, dT is defined by: d if d ∈ T succT(d) otherwise We introduce the technical notions of derivative dataflow and derivative function that will be useful to build final systems.
Systems as coalgebras
We now rewrite our definition of systems from Chapter 3 using our coalgebraic formalism:
Definition 5.1.8 (Systems) Let In and Out be two datasets denoting, respec-tively, the values in inputs and outputs. Let T be a time reference. A system S is defined by a coalgebra (S, ) for the signature H = (Out )In T : Set → Set where T T is the time scale of S, together with a distinguished element q0 denoting the initial state of the system S. A system S is called a pre-system when its initial state is removed.
Any deterministic Mealy machine can be represented in our formalism. In-deed, given a Mealy machine (S, ) with : S → (Out S)In, we can define the equivalent pre-system S = (S, ′) over the signature (Out )In ω by: ∀n < ω, ∀i ∈ In, ∀q ∈ Q, ′(q)(i, n) = (q)(i). More generally, all examples of systems from Chapter 3 can be easily translated to our coalgebraic formalism. In the following, given a system ((S, ), qo) over a signature H = (Out )In T, we will note (q)(i, d)1 (resp. (q)(i, d)2 ) the resulting output value (resp. resulting state) of the pair (q)(i, d). Definition 5.1.9 (Category of systems) Let S = ((S, ), q0) and S′ = ((S′, ′), q′ ) be two systems over H. A system morphism h : S → S′ is a 0 ) → (S′, ′) such that h(q0) = h(q′ ). coalgebra homomorphism h : (S, 0 We note Sys(H) (resp. P Sys(H)) the category of systems (resp. of pre-systems) over H.
Table of contents :
1 Introduction
1.1 Complex industrial systems
1.2 Systems Engineering
1.3 What is systems architecture?
1.3.1 A definition
1.3.2 Fundamental principles
1.4 Towards a unified formalism
1.5 Structure of this manuscript
I Systemsmodeling
2 Heterogeneousdataflows
2.1 Time
2.1.1 Time reference
2.1.2 Time scale
2.2 Data
2.2.1 Datasets
2.2.2 Implementation of standard data behaviors
2.3 Dataflows
2.3.1 Definition
2.3.2 Operators
2.3.3 Consistency of dataflows
3 Systems
3.1 Systems
3.1.1 Definition
3.1.2 Execution
3.1.3 Examples & expressivity
3.2 Transfer functions
3.2.1 Definition
3.2.2 Transfer function of a system
4 Integration operators
4.1 Composition
4.1.1 Timed extension
4.1.2 Product
4.1.3 Feedback
4.2 Abstraction
4.2.1 Nondeterminism
4.2.2 Abstraction
4.3 Integration of systems
4.3.1 Composition & abstraction
4.3.2 Example
II Systems architecture
5 Alogic for requirements
5.1 A coalgebraic definition of systems
5.1.1 Preliminaries
5.1.2 Transfer functions via coalgebras
5.1.3 Systems as coalgebras
5.2 A logic for system requirements
5.2.1 Definition
5.2.2 Examples of requirements
5.2.3 Adequacy of the logic
6 Towards a framework for system sarchitecture
6.1 Handling underspecification
6.2 Modeling recursive structure
7 Fair assignments between systems
7.1 Introduction
7.2 Inequality measurement with Lorenz dominance relations
7.2.1 Notations and definitions
7.2.2 Infinite order Lorenz dominance
7.3 Properties of infinite order Lorenz dominance
7.3.1 A representation theorem
7.3.2 Main properties of L∞-dominance
7.4 Solving multiagent assignment problems
7.4.1 Fair multiagent optimization
7.4.2 Linearization of the problem
7.4.3 Numerical tests
8 Conclusion
