Abstract
The main subject of our investigation is behaviour of the continuous components of hybrid systems. By a hybrid system we mean a network of digital and analog devices interacting at discrete times. A first-order logical formalization of hybrid systems is proposed in which the trajectories of the continuous components are presented by majorant-computable functionals.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Backus, Can Programming be Liberated from the von Neumann Style, A Functional Style and its Algebra of Programs, Comm. of the ACM, V. 21, N 8, 1978, pages 613–642.
J. Barwise, Admissible sets and structures, Berlin, Springer-Verlag, 1975.
L. Blum and M. Shub and S. Smale, On a theory of computation and complexity over the reals:NP-completeness, recursive functions and universal machines, Bull. Amer. Math. Soc., (N.S.), v. 21, no. 1, 1989, pages 1–46.
A. Edalat, P. Sünderhauf, A domain-theoretic approach to computability on the real line, Theoretical Computer Science. To appear.
Yu. L. Ershov, Definability and computability, Plenum, New York, 1996.
H. Freedman and K. Ko, Computational complexity of real functions, Theoret. Comput. Sci., v. 20, 1982, pages 323–352.
A Logical for specification of Continuous System, LNCS N 1386, 1998, pages 143–159.
S.S. Goncharov, D.I. Sviridenko, Σ-programming, Vychislitel’nye Sistemy, Novosibirsk, v. 107, 1985, pages 3–29.
A. Grzegorczyk, On the definitions of computable real continuous functions, Fund. Math., N 44, 1957, pages 61–71.
T.A. Henzinger, Z. Manna, A. Pnueli, Towards refining Temporal Specifications into Hybrid Systems, LNCS N 736, 1993, pages 36–60.
T.A. Henzinger, V. Rusu, Reachability Verification for Hybrid Automata, LNCS N 1386, 1998, pages 190–205.
M. Korovina, Generalized computability of real functions, Siberian Advance of Mathematics, v. 2, N 4, 1992, pages 1–18.
M. Korovina, O. Kudinov, A New Approach to Computability over the Reals, SibAM, v. 8, N 3, 1998, pages 59–73.
M. Korovina, O. Kudinov, Characteristic Properties of Majorant-Computability over the Reals, Proc. of CSL’98, LNCS, to appear.
C. Livadas, N.A. Lynch, Formal verification of Safety-Critical hybrid systems, LNCS N 1386, 1998, pages 253–273.
Z. Manna, A. Pnueli, Verifying Hybrid Systems, LNCS N 736, 1993, pages 4–36.
R. Montague, Recursion theory as a branch of model theory, Proc. of the third international congr. on Logic, Methodology and the Philos. of Sc., 1967, Amsterdam, 1968, pages 63–86.
Y. N. Moschovakis, Abstract first order computability, Trans. Amer. Math. Soc., v. 138, 1969, pages 427–464.
A. Nerode, W. Kohn Models for Hybrid Systems: Automata, Topologies, Controllability, Observability, LNCS N 736, 1993, pages 317–357.
M. B. Pour-El, J. I. Richards, Computability in Analysis and Physics, Springer-Verlag, 1988.
D. Scott, Outline of a mathematical theory of computation, In 4th Annual Princeton Conference on Information Sciences and Systems, 1970, pages 169–176.
V. Stoltenberg-Hansen and J. V. Tucker, Effective algebras, Handbook of Logic in computer Science, v. 4, Clarendon Press, 1995, pages 375–526.
B.A. Trakhtenbrot, Yu. Barzdin, Finite automata: Behaviour and Syntheses, North-Holland, 1973.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Korovina, M.V., Kudinov, O.V. (2000). A Logical Approach to Specification of Hybrid Systems. In: Bjøner, D., Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 1999. Lecture Notes in Computer Science, vol 1755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46562-6_2
Download citation
DOI: https://doi.org/10.1007/3-540-46562-6_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67102-2
Online ISBN: 978-3-540-46562-1
eBook Packages: Springer Book Archive