Hybrid Techniques for Hybrid Systems

T. Krilavicius

Abstract

Computer controlled systems are almost omnipresent nowadays. We expect such systems to function properly at any time we need them. The malfunctioning of home electronics just irritates us, but glitches in a car, power plant or medical support system may threaten life, and faults in nuclear missile control facility may bring the end to civilisation. Such ubiquity of computer-based control puts very high reliability requirements on such systems. Hybrid systems combine continuous real-time behaviour and discrete events. Research in hybrid systems aims at providing means for reliable design and production of hybrid systems. In this thesis, we explore the world of hybrid systems. We acknowledge relevance and complexity of hybrid systems research, and emphasise several different research topics: modelling, analysis, testing and deployment of hybrid systems. We illustrate hybrid systems by presenting a collection of examples that reflect hybrid phenomena, its variety and occurrence in different applications. Of course, the list is not exhaustive, because only illustrative examples were chosen. However, it represents the diversity of hybrid systems sufficiently well to reveal the size and complexity of problems, and the broadness of the application area. We survey several major formalisms for modelling and analysis of hybrid systems. We overview an existing classification of hybrid systems, and propose a generalised classification scheme for diverse frameworks. Moreover, we classify the surveyed formalisms according to the proposed scheme. We propose a technique for stability estimation for a certain class of hybrid automata. It combines ideas from computer science and control theory, and is based on cycles detection and conservative gains estimation. We borrow the well-known algorithm for transforming a finite automaton into an equivalent regular expression for cycles detection from computer science. From control theory, we take the idea of conservative gains and use them to estimate stability of cycles. We introduce Behavioural Hybrid Process Calculus (BHPC), a formalism for modelling and analysis of hybrid systems. It combines process algebraic techniques and the behavioural approach [Polderman and Willems, 1998] to dynamical systems. We take an attempt to advance fusion of computer science and control theory in hybrid systems research. BHPC is based on two fundamental notions of actions and trajectories that describe discrete and continuous evolution of dynamical systems, respectively. At a higher abstraction level these two types of behaviour are treated uniformly, i.e., as normal elements of process algebra. Their behaviour is defined using structural operational semantics (SOS) rules [Plotkin, 1981, 2003]. Moreover, the rules already respect the differences between trajectory prefixes and action prefixes, based on our intuition on how such processes should behave. For example, in parallel composition trajectory prefixes are always required to synchronise, while for action prefixes interleaving semantics is adopted. Furthermore, we define a hybrid strong bisimulation relation for BHPC and prove that it is congruence. It is one of the most important properties to attain well-defined compositionality. Such a property allows interchanging bisimilar processes in any process algebraic expression. In other words, it allows refining process, changing their internal representation, and interchanging them without any losses as long as they manifest the same behaviour. We propose a technique for simulation of BHPC. We devise a simulation algorithm for a subset of BHPC operators and test some of the proposed techniques in the BHAVE prototype. The proposed simulation algorithm defines one of the possible ways to simulate Behavioural Hybrid Process Calculus. Moreover, we survey the major problems in simulation of hybrid systems in the light of BHPC and in a more general layout. For some of the issues we propose solutions, for the remaining we discuss potential ways to tackle the problems.
Original languageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Brinksma, Hendrik , Supervisor
  • Langerak, Romanus , Advisor
Sponsors
Date of Award6 Sep 2006
Place of PublicationEnschede
Publisher
Print ISBNs90-365-2397-4
StatePublished - 6 Sep 2006

Fingerprint

Hybrid systems
Control theory
Computer science
Computer control
Trajectories
Dynamical systems
Semantics
Control facilities
Finite automata
Set theory
Missiles
Algebra
Refining
Mathematical operators
Power plants
Electronic equipment
Railroad cars
Fusion reactions

Keywords

  • METIS-239016
  • EWI-9609
  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • IR-57124

Cite this

Krilavicius, T. (2006). Hybrid Techniques for Hybrid Systems Enschede: Centre for Telematics and Information Technology (CTIT)
Krilavicius, T.. / Hybrid Techniques for Hybrid Systems. Enschede : Centre for Telematics and Information Technology (CTIT), 2006. 192 p.
@misc{ac231b2574424fb585cef41416f24218,
title = "Hybrid Techniques for Hybrid Systems",
abstract = "Computer controlled systems are almost omnipresent nowadays. We expect such systems to function properly at any time we need them. The malfunctioning of home electronics just irritates us, but glitches in a car, power plant or medical support system may threaten life, and faults in nuclear missile control facility may bring the end to civilisation. Such ubiquity of computer-based control puts very high reliability requirements on such systems. Hybrid systems combine continuous real-time behaviour and discrete events. Research in hybrid systems aims at providing means for reliable design and production of hybrid systems. In this thesis, we explore the world of hybrid systems. We acknowledge relevance and complexity of hybrid systems research, and emphasise several different research topics: modelling, analysis, testing and deployment of hybrid systems. We illustrate hybrid systems by presenting a collection of examples that reflect hybrid phenomena, its variety and occurrence in different applications. Of course, the list is not exhaustive, because only illustrative examples were chosen. However, it represents the diversity of hybrid systems sufficiently well to reveal the size and complexity of problems, and the broadness of the application area. We survey several major formalisms for modelling and analysis of hybrid systems. We overview an existing classification of hybrid systems, and propose a generalised classification scheme for diverse frameworks. Moreover, we classify the surveyed formalisms according to the proposed scheme. We propose a technique for stability estimation for a certain class of hybrid automata. It combines ideas from computer science and control theory, and is based on cycles detection and conservative gains estimation. We borrow the well-known algorithm for transforming a finite automaton into an equivalent regular expression for cycles detection from computer science. From control theory, we take the idea of conservative gains and use them to estimate stability of cycles. We introduce Behavioural Hybrid Process Calculus (BHPC), a formalism for modelling and analysis of hybrid systems. It combines process algebraic techniques and the behavioural approach [Polderman and Willems, 1998] to dynamical systems. We take an attempt to advance fusion of computer science and control theory in hybrid systems research. BHPC is based on two fundamental notions of actions and trajectories that describe discrete and continuous evolution of dynamical systems, respectively. At a higher abstraction level these two types of behaviour are treated uniformly, i.e., as normal elements of process algebra. Their behaviour is defined using structural operational semantics (SOS) rules [Plotkin, 1981, 2003]. Moreover, the rules already respect the differences between trajectory prefixes and action prefixes, based on our intuition on how such processes should behave. For example, in parallel composition trajectory prefixes are always required to synchronise, while for action prefixes interleaving semantics is adopted. Furthermore, we define a hybrid strong bisimulation relation for BHPC and prove that it is congruence. It is one of the most important properties to attain well-defined compositionality. Such a property allows interchanging bisimilar processes in any process algebraic expression. In other words, it allows refining process, changing their internal representation, and interchanging them without any losses as long as they manifest the same behaviour. We propose a technique for simulation of BHPC. We devise a simulation algorithm for a subset of BHPC operators and test some of the proposed techniques in the BHAVE prototype. The proposed simulation algorithm defines one of the possible ways to simulate Behavioural Hybrid Process Calculus. Moreover, we survey the major problems in simulation of hybrid systems in the light of BHPC and in a more general layout. For some of the issues we propose solutions, for the remaining we discuss potential ways to tackle the problems.",
keywords = "METIS-239016, EWI-9609, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, IR-57124",
author = "T. Krilavicius",
year = "2006",
month = "9",
isbn = "90-365-2397-4",
publisher = "Centre for Telematics and Information Technology (CTIT)",
address = "Netherlands",
school = "University of Twente",

}

Krilavicius, T 2006, 'Hybrid Techniques for Hybrid Systems', University of Twente, Enschede.

Hybrid Techniques for Hybrid Systems. / Krilavicius, T.

Enschede : Centre for Telematics and Information Technology (CTIT), 2006. 192 p.

Research output: ScientificPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Hybrid Techniques for Hybrid Systems

AU - Krilavicius,T.

PY - 2006/9/6

Y1 - 2006/9/6

N2 - Computer controlled systems are almost omnipresent nowadays. We expect such systems to function properly at any time we need them. The malfunctioning of home electronics just irritates us, but glitches in a car, power plant or medical support system may threaten life, and faults in nuclear missile control facility may bring the end to civilisation. Such ubiquity of computer-based control puts very high reliability requirements on such systems. Hybrid systems combine continuous real-time behaviour and discrete events. Research in hybrid systems aims at providing means for reliable design and production of hybrid systems. In this thesis, we explore the world of hybrid systems. We acknowledge relevance and complexity of hybrid systems research, and emphasise several different research topics: modelling, analysis, testing and deployment of hybrid systems. We illustrate hybrid systems by presenting a collection of examples that reflect hybrid phenomena, its variety and occurrence in different applications. Of course, the list is not exhaustive, because only illustrative examples were chosen. However, it represents the diversity of hybrid systems sufficiently well to reveal the size and complexity of problems, and the broadness of the application area. We survey several major formalisms for modelling and analysis of hybrid systems. We overview an existing classification of hybrid systems, and propose a generalised classification scheme for diverse frameworks. Moreover, we classify the surveyed formalisms according to the proposed scheme. We propose a technique for stability estimation for a certain class of hybrid automata. It combines ideas from computer science and control theory, and is based on cycles detection and conservative gains estimation. We borrow the well-known algorithm for transforming a finite automaton into an equivalent regular expression for cycles detection from computer science. From control theory, we take the idea of conservative gains and use them to estimate stability of cycles. We introduce Behavioural Hybrid Process Calculus (BHPC), a formalism for modelling and analysis of hybrid systems. It combines process algebraic techniques and the behavioural approach [Polderman and Willems, 1998] to dynamical systems. We take an attempt to advance fusion of computer science and control theory in hybrid systems research. BHPC is based on two fundamental notions of actions and trajectories that describe discrete and continuous evolution of dynamical systems, respectively. At a higher abstraction level these two types of behaviour are treated uniformly, i.e., as normal elements of process algebra. Their behaviour is defined using structural operational semantics (SOS) rules [Plotkin, 1981, 2003]. Moreover, the rules already respect the differences between trajectory prefixes and action prefixes, based on our intuition on how such processes should behave. For example, in parallel composition trajectory prefixes are always required to synchronise, while for action prefixes interleaving semantics is adopted. Furthermore, we define a hybrid strong bisimulation relation for BHPC and prove that it is congruence. It is one of the most important properties to attain well-defined compositionality. Such a property allows interchanging bisimilar processes in any process algebraic expression. In other words, it allows refining process, changing their internal representation, and interchanging them without any losses as long as they manifest the same behaviour. We propose a technique for simulation of BHPC. We devise a simulation algorithm for a subset of BHPC operators and test some of the proposed techniques in the BHAVE prototype. The proposed simulation algorithm defines one of the possible ways to simulate Behavioural Hybrid Process Calculus. Moreover, we survey the major problems in simulation of hybrid systems in the light of BHPC and in a more general layout. For some of the issues we propose solutions, for the remaining we discuss potential ways to tackle the problems.

AB - Computer controlled systems are almost omnipresent nowadays. We expect such systems to function properly at any time we need them. The malfunctioning of home electronics just irritates us, but glitches in a car, power plant or medical support system may threaten life, and faults in nuclear missile control facility may bring the end to civilisation. Such ubiquity of computer-based control puts very high reliability requirements on such systems. Hybrid systems combine continuous real-time behaviour and discrete events. Research in hybrid systems aims at providing means for reliable design and production of hybrid systems. In this thesis, we explore the world of hybrid systems. We acknowledge relevance and complexity of hybrid systems research, and emphasise several different research topics: modelling, analysis, testing and deployment of hybrid systems. We illustrate hybrid systems by presenting a collection of examples that reflect hybrid phenomena, its variety and occurrence in different applications. Of course, the list is not exhaustive, because only illustrative examples were chosen. However, it represents the diversity of hybrid systems sufficiently well to reveal the size and complexity of problems, and the broadness of the application area. We survey several major formalisms for modelling and analysis of hybrid systems. We overview an existing classification of hybrid systems, and propose a generalised classification scheme for diverse frameworks. Moreover, we classify the surveyed formalisms according to the proposed scheme. We propose a technique for stability estimation for a certain class of hybrid automata. It combines ideas from computer science and control theory, and is based on cycles detection and conservative gains estimation. We borrow the well-known algorithm for transforming a finite automaton into an equivalent regular expression for cycles detection from computer science. From control theory, we take the idea of conservative gains and use them to estimate stability of cycles. We introduce Behavioural Hybrid Process Calculus (BHPC), a formalism for modelling and analysis of hybrid systems. It combines process algebraic techniques and the behavioural approach [Polderman and Willems, 1998] to dynamical systems. We take an attempt to advance fusion of computer science and control theory in hybrid systems research. BHPC is based on two fundamental notions of actions and trajectories that describe discrete and continuous evolution of dynamical systems, respectively. At a higher abstraction level these two types of behaviour are treated uniformly, i.e., as normal elements of process algebra. Their behaviour is defined using structural operational semantics (SOS) rules [Plotkin, 1981, 2003]. Moreover, the rules already respect the differences between trajectory prefixes and action prefixes, based on our intuition on how such processes should behave. For example, in parallel composition trajectory prefixes are always required to synchronise, while for action prefixes interleaving semantics is adopted. Furthermore, we define a hybrid strong bisimulation relation for BHPC and prove that it is congruence. It is one of the most important properties to attain well-defined compositionality. Such a property allows interchanging bisimilar processes in any process algebraic expression. In other words, it allows refining process, changing their internal representation, and interchanging them without any losses as long as they manifest the same behaviour. We propose a technique for simulation of BHPC. We devise a simulation algorithm for a subset of BHPC operators and test some of the proposed techniques in the BHAVE prototype. The proposed simulation algorithm defines one of the possible ways to simulate Behavioural Hybrid Process Calculus. Moreover, we survey the major problems in simulation of hybrid systems in the light of BHPC and in a more general layout. For some of the issues we propose solutions, for the remaining we discuss potential ways to tackle the problems.

KW - METIS-239016

KW - EWI-9609

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - IR-57124

M3 - PhD Thesis - Research UT, graduation UT

SN - 90-365-2397-4

PB - Centre for Telematics and Information Technology (CTIT)

ER -

Krilavicius T. Hybrid Techniques for Hybrid Systems. Enschede: Centre for Telematics and Information Technology (CTIT), 2006. 192 p.