From physical modelling to compositional models of hybrid systems

  • Simin Nadjm-Tehrani
  • Jan-Erik Strömberg
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 863)


By a hybrid system we mean a discrete controller in interaction with a physical environment. This paper discusses methodologies for incorporating physically grounded models in representations of hybrid systems. To this end, we study a driver support system, an example which includes unmodelled inputs. We consider models at different levels of abstraction. First, we show that discrete models of the environment can be obtained from the continuous models without losing relevant information. We do this using an analysis of the continuous state space. Dynamic Transition Systems (DTS) are used for the modular modelling at this level of abstraction. Next, we consider models using Hybrid Transition Systems (HTS). This can be seen as a modular version of timed transition systems allowing both differential and algebraic equations in each mode. Finally, we comment on expressivity requirements on hybrid formalisms for modelling realistic physical systems.


Model Check Hybrid System Transition System Temporal Logic Discrete Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi and L. Lamport. An Old-Fashioned Recipe for Real-Time. In de Bakker et al. [7], pages 1–27.Google Scholar
  2. 2.
    R. Alur, C. Courcoubetis, and D. Dill. Model-checking for Real-Time Systems. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 414–425. Computer Society Press, 1990.Google Scholar
  3. 3.
    R. Alur, T.A. Henzinger, and P.H. Ho. Automatic Symbolic Verification of Embedded Systems. In Proc. of Real Time Systems Symposium. Computer Society Press, 1993.Google Scholar
  4. 4.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proc. IEEE Conf. on Logic in Computer Science, pages 428–439. Computer Society Press, 1990.Google Scholar
  5. 5.
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986. An early version of the paper appeared at the 10th ACM symposium on principles of programming languages, 1983.Google Scholar
  6. 6.
    E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another Look at LTL Model Checking. In Proc. 6th Int. Conf. on Computer Aided Verification (CAV'94). Springer Verlag, 1994.Google Scholar
  7. 7.
    J.W. de Bakker, C. Huizing, W.P. de Roever, and G.Rozenberg, editors. Proc. REX workshop 1991. Springer Verlag, LNCS 600, 1992.Google Scholar
  8. 8.
    E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative Temporal Reasoning. Real-Time Systems, 4:331–352, 1992. An early version of the paper appeared at the workshop on automatic verification methods for finite state systems, Grenoble, 1989.Google Scholar
  9. 9.
    R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors. Proc. Workshop on Theory of Hybrid Systems, October 1992, LNCS 736, Lyngby, Denmark, 1993. Springer Verlag.Google Scholar
  10. 10.
    E. Harel, O. Lichtenstein, and A. Pnueli. Explicit Clock Temporal Logic. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 402–413. Computer Society Press, 1990.Google Scholar
  11. 11.
    T.A. Henzinger, Z. Manna, and A. Pnueli. Temporal Proof Methodologies for Real-Time Systems. In 18th ACM Symp. on Principles of Programming Languages, pages 353–366, 1991.Google Scholar
  12. 12.
    T.A Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-time Systems. In proceedings of IEEE Symposium on Logic in Computer Science, pages 394–406. Computer Society Press, 1992.Google Scholar
  13. 13.
    R. Kaivola. Compositional Model Checking for Linear-Time Temporal Logic. In Proc. 4th int. workshop on Computer Aided Verification, pages 248–259. Springer Verlag, 1992.Google Scholar
  14. 14.
    D.C. Karnopp, R.C. Rosenberg, and D. Margolis. System dynamics — A unified approach (2nd edition). John Wiley & Sons, New York, 1990.Google Scholar
  15. 15.
    Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In Grossman et al.[9], pages 179–208.Google Scholar
  16. 16.
    D. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, School of Computer Science, Carnegie Mellon University, July 1993. CMU-CS-93-178.Google Scholar
  17. 17.
    N. Lynch and F. Vaandrager. Forward and Backward Simulations, Part I: Untimed Systems. Technical Report MIT/LCS/TM-486, Laboratory for Computer science, MIT, May 1993.Google Scholar
  18. 18.
    N. Lynch and F. Vaandrager. Forward and Backward Simulations, Part II: Timing-based Systems. Technical Report MIT/LCS/TM-487, Laboratory for Computer science, MIT, May 1993.Google Scholar
  19. 19.
    O. Maler, Z. Manna, and A. Pnueli. From Timed to Hybrid Systems. In de Bakker et al. [7], pages 447–484.Google Scholar
  20. 20.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems — volume I. Springer Verlag, 1991.Google Scholar
  21. 21.
    Z. Manna and A. Pnueli. Verifying Hybrid Systems. In Grossman et al.[9], pages 4–35.Google Scholar
  22. 22.
    K. Marzullo, F. B. Schneider, and N. Budhiraja. Derivation of Sequential, Real-time, Process Control Programs. In A.M. van Tilborg and G.M. Koob, editors, Foundations of Real-Time Computing, Volume I: Formal Specifications and Methods, pages 39–54. Kluwer Academic Publishers, 1991.Google Scholar
  23. 23.
    M. Morin, S. Nadjm-Tehrani, P. österling, and E. Sandewall. Real-Time Hierarchical Control. IEEE Software, 9(5):51–57, September 1992.Google Scholar
  24. 24.
    S. Nadjm-Tehrani. Reactive Systems in Physical Environments: Compositional Modelling and Framework for Verification. PhD thesis, Dept. of Computer and Information Science, Linköping University, March 1994. Dissertation No. 338.Google Scholar
  25. 25.
    X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An Approach to Description and Analysis of Hybrid Systems. In Grossman et al. [9], pages 149–178.Google Scholar
  26. 26.
    J. S. Ostroff. Temporal Logic for Real-Time Systems. Research Studies Press Ltd., Somerset, 1989.Google Scholar
  27. 27.
    J. S. Ostroff. Deciding Properties of Timed Transition Models. IEEE Transactions on Parallel and Distributed Systems, 1(2):170–183, April 1990.Google Scholar
  28. 28.
    H. M. Paynter. Analysis and design of engineering systems. MIT Press, Cambridge, Mass., 1961.Google Scholar
  29. 29.
    A. P. Ravn and H. Rischel. Requirements Capture for Embedded Real-Time Systems. In IMACS-IFAC Symposium: Modelling and Control of Technological Systems. IMACS, May 1991.Google Scholar
  30. 30.
    E. Sandewall. Combining Logic and Differential Equations for Describing Realworld Systems. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence (IJCAI'89), Detroit, pages 412–420. Morgan. Kaufman, 1989.Google Scholar
  31. 31.
    E.D. Sontag. Nonlinear regulation: the piecewise linear approach. IEEE Trans. on Automatic Control, 26(2), April 1981.Google Scholar
  32. 32.
    J.A. Stiver and P.J. Antsaklis. Modeling and Analysis of Hybrid Systems. In Proc. of the 31st IEEE Conf. on Decision and Control (CDC '92), pages 3748–3751, Tucson, 1992.Google Scholar
  33. 33.
    J.E. Strömberg and S. Nadjm-Tehrani. On Discrete and Hybrid Representation of Hybrid Systems. In Proceedings of the SCS International Conference on Modeling and Simulation (ESM '94), pages 1085–1089, Barcelona, June 1994.Google Scholar
  34. 34.
    J.E. Strömberg, J. Top, and U. Söderman. Variable causality in bond graphs caused by discrete effects. In Proc. First Int. Conf. on Bond Graph Modeling (ICBGM '93), number 2 in SCS Simulation Series, volume 25, pages 115–119, San Diego, 1993.Google Scholar
  35. 35.
    F. Wang, A.K. Mok, and E. A. Emerson. Symbolic Model Checking for Distributed Real-Time Systems. In J.C.P. Woodcock and P.G. Larsen, editors, Proceedings of the first Int. Symposium of Formal Methods Europe, FME'93: Industrial-Strength Formal Methods, pages 632–651. Springer Verlag, 1993.Google Scholar
  36. 36.
    D. S. Weld and J. de Kleer, editors. Readings in Qualitative Reasoning about Physical Systems. Morgan Kaufman, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Simin Nadjm-Tehrani
    • 1
  • Jan-Erik Strömberg
    • 2
  1. 1.Dept. of Computer and Information ScienceLinköping UniversitySweden
  2. 2.Div. of Automatic Control, Dept. of Electrical EngineeringLinköping UniversityLinköpingSweden

Personalised recommendations