×

The fixed-point theory of strictly causal functions. (English) Zbl 1318.68116

Summary: We ask whether strictly causal components form well defined systems when arranged in feedback configurations. The standard interpretation for such configurations induces a fixed-point constraint on the function modeling the component involved. We define strictly causal functions formally, and show that the corresponding fixed-point problem does not always have a well defined solution. We examine the relationship between these functions and the functions that are strictly contracting with respect to a generalized distance function on signals, and argue that these strictly contracting functions are actually the functions that one ought to be interested in. We prove a constructive fixed-point theorem for these functions, introduce a corresponding induction principle, and study the related convergence process.

MSC:

68Q55 Semantics in the theory of computing
06B35 Continuous lattices and posets, applications
54H25 Fixed-point and coincidence theorems (topological aspects)
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

Software:

SysML; SystemC; Esterel
PDFBibTeX XMLCite
Full Text: DOI

References:

[4] Abadi, Martín; Lamport, Leslie, An old-fashioned recipe for real time, (de Bakker, J.; Huizing, C.; de Roever, W.; Rozenberg, G., Real-Time: Theory in Practice. Real-Time: Theory in Practice, Lecture Notes in Computer Science, vol. 600 (1992), Springer: Springer Berlin/Heidelberg), 1-27
[5] Alur, Rajeev; Courcoubetis, Constantin; Dill, David, Model-checking for real-time systems, (Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science. Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, June 1990, LICS ’90 (1990)), 414-425
[6] Alur, Rajeev; Henzinger, Thomas, Logics and models of real time: a survey, (de Bakker, J.; Huizing, C.; de Roever, W.; Rozenberg, G., Real-Time: Theory in Practice. Real-Time: Theory in Practice, Lecture Notes in Computer Science, vol. 600 (1992), Springer: Springer Berlin/Heidelberg), 74-106 · Zbl 1512.68146
[8] Broy, Manfred, Refinement of time, Theoret. Comput. Sci., 253, 1, 3-26 (2001) · Zbl 0954.68097
[9] Caspi, Paul; Benveniste, Albert; Lublinerman, Roberto; Tripakis, Stavros, Actors without directors: a Kahnian view of heterogeneous systems, (Majumdar, Rupak; Tabuada, Paulo, Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 5469 (2009), Springer: Springer Berlin/Heidelberg), 46-60 · Zbl 1237.68122
[10] Cataldo, Adam; Lee, Edward A.; Liu, Xiaojun; Matsikoudis, Eleftherios; Zheng, Haiyang, A constructive fixed-point theorem and the feedback semantics of timed systems, (2006 8th International Workshop on Discrete Event Systems (July 2006)), 27-32
[11] Cousot, Patrick; Cousot, Radhia, Constructive versions of Tarski’s fixed point theorems, Pacific J. Math., 82, 1, 43-57 (1979) · Zbl 0413.06004
[12] Davey, Brian A.; Priestley, Hilary A., Introduction to Lattices and Order (2002), Cambridge University Press · Zbl 1002.06001
[13] Dummett, Michael, Causal loops, (Flood, Raymond; Lockwood, Michael, The Nature of Time (1986), Basil Blackwell), 135-169, Chap. 9
[14] Eidson, John C.; Lee, Edward A.; Matic, Slobodan; Seshia, Sanjit A.; Zou, Jia, Distributed real-time software for cyber-physical systems, Proc. IEEE, 100, 1, 45-59 (January 2012)
[15] Enderton, Herbert B., Elements of Set Theory (1977), Academic Press · Zbl 0383.03034
[16] Feiler, Peter H.; Gluch, David P.; Hudak, John J., The Architecture Analysis & Design Language (AADL): an introduction (February 2006), Software Engineering Institute, Carnegie Mellon University, Technical Note CMU/SEI-2006-TN-011
[17] Godskesen, Jens Chr.; Larsen, Kim G., Real-time calculi and expansion theorems, (Shyamasundar, Rudrapatna, Foundations of Software Technology and Theoretical Computer Science. Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 652 (1992), Springer: Springer Berlin/Heidelberg), 302-315
[18] Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir, Timed transition systems, (de Bakker, J.; Huizing, C.; de Roever, W.; Rozenberg, G., Real-Time: Theory in Practice. Real-Time: Theory in Practice, Lecture Notes in Computer Science, vol. 600 (1992), Springer: Springer Berlin/Heidelberg), 226-251
[19] Hesselink, Wim H., A generalization of Naundorf’s fixpoint theorem, Theoret. Comput. Sci., 247, 1-2, 291-296 (2000) · Zbl 0949.68095
[20] Hitzler, Pascal, Generalized metrics and topology in logic programming semantics (2001), Department of Mathematics, National University of Ireland, University College Cork, PhD thesis
[21] Hitzler, Pascal; Seda, Anthony Karel, The fixed-point theorems of Priess-Crampe and Ribenboim in logic programming, (Kuhlmann, Franz-Viktor; Kuhlmann, Salma; Marshall, Murray, Valuation Theory and Its Applications, Proceedings of the 1999 Valuation Theory Conference. Valuation Theory and Its Applications, Proceedings of the 1999 Valuation Theory Conference, University of Saskatchewan in Saskatoon, Canada. Valuation Theory and Its Applications, Proceedings of the 1999 Valuation Theory Conference. Valuation Theory and Its Applications, Proceedings of the 1999 Valuation Theory Conference, University of Saskatchewan in Saskatoon, Canada, Fields Institute Communications, vol. 32 (2002), American Mathematical Society), 219-235 · Zbl 1005.68177
[22] Hitzler, Pascal; Seda, Anthony Karel, Generalized metrics and uniquely determined logic programs, Theoret. Comput. Sci., 305, 1-3, 187-219 (2003) · Zbl 1071.68018
[23] Jacques, Vincent; Wu, E.; Grosshans, Frédéric; Treussart, François; Grangier, Philippe; Aspect, Alain; Roch, Jean-François, Experimental realization of Wheeler’s delayed-choice gedanken experiment, Science, 315, 5814, 966-968 (2007)
[24] Kahn, Gilles, The semantics of a simple language for parallel programming, (Rosenfeld, J. L., Information Processing ’74: Proceedings of the IFIP Congress (August 1974), North-Holland Publishing Company: North-Holland Publishing Company Stockholm, Sweden), 471-475 · Zbl 0299.68007
[25] Kozen, Dexter; Ruozzi, Nicholas, Applications of metric coinduction, (CALCO’07: Proceedings of the 2nd International Conference on Algebra and Coalgebra in Computer Science (2007), Springer-Verlag: Springer-Verlag Berlin/Heidelberg), 327-341 · Zbl 1214.68218
[26] Krötzsch, Markus, Generalized ultrametric spaces in quantitative domain theory, Theoret. Comput. Sci., 368, 1-2, 30-49 (2006) · Zbl 1171.68542
[27] Lee, Edward A., Modeling concurrent real-time processes using discrete events, Ann. Softw. Eng., 7, 1, 25-45 (1999)
[28] Lee, Edward A.; Sangiovanni-Vincentelli, Alberto, A framework for comparing models of computation, IEEE Trans. Comput. Aided Design Integr. Circuits Syst., 17, 12, 1217-1229 (December 1998)
[29] Lee, Edward A.; Varaiya, Pravin, Structure and Interpretation of Signals and Systems (2011)
[30] Liu, Jie; Lee, Edward, On the causality of mixed-signal and hybrid models, (Maler, Oded; Pnueli, Amir, Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 2623 (2003), Springer: Springer Berlin/Heidelberg), 328-342 · Zbl 1032.93534
[31] Liu, Xiaojun, Semantic foundation of the tagged signal model (December 2005), EECS Department, University of California: EECS Department, University of California Berkeley, PhD thesis
[32] Liu, Xiaojun; Lee, Edward A., CPO semantics of timed interactive actor networks, Theoret. Comput. Sci., 409, 1, 110-125 (2008) · Zbl 1157.68046
[33] Liu, Xiaojun; Matsikoudis, Eleftherios; Lee, Edward A., Modeling timed concurrent systems, (Baier, Christel; Hermanns, Holger, CONCUR 2006 - Concurrency Theory. CONCUR 2006 - Concurrency Theory, Lecture Notes in Computer Science, vol. 4137 (2006), Springer: Springer Berlin/Heidelberg), 1-15 · Zbl 1151.68543
[34] Liu, Xiaojun; Matsikoudis, Eleftherios; Lee, Edward A., Modeling timed concurrent systems using generalized ultrametrics (May 2006), EECS Department, University of California: EECS Department, University of California Berkeley, Technical report UCB/EECS-2006-45
[35] Maler, Oded; Manna, Zohar; Pnueli, Amir, From timed to hybrid systems, (de Bakker, J.; Huizing, C.; de Roever, W.; Rozenberg, G., Real-Time: Theory in Practice. Real-Time: Theory in Practice, Lecture Notes in Computer Science, vol. 600 (1992), Springer: Springer Berlin/Heidelberg), 447-484
[36] Markowsky, George, Chain-complete posets and directed sets with applications, Algebra Universalis, 6, 1, 53-68 (1976) · Zbl 0332.06001
[37] Matsikoudis, Eleftherios; Lee, Edward A., From transitions to executions, (Pattinson, Dirk; Schröder, Lutz, Coalgebraic Methods in Computer Science. Coalgebraic Methods in Computer Science, Lecture Notes in Computer Science, vol. 7399 (2012), Springer: Springer Berlin/Heidelberg), 170-190 · Zbl 1318.68122
[38] Matsikoudis, Eleftherios; Lee, Edward A., Labelled execution systems (May 2012), EECS Department, University of California: EECS Department, University of California Berkeley, Technical report UCB/EECS-2012-64
[39] Matsikoudis, Eleftherios; Lee, Edward A., An axiomatization of the theory of generalized ultrametric semilattices of linear signals, (Gąsieniec, Leszek; Wolter, Frank, Fundamentals of Computation Theory. Fundamentals of Computation Theory, Lecture Notes in Computer Science, vol. 8070 (2013), Springer: Springer Berlin/Heidelberg), 248-258 · Zbl 1318.68115
[40] Matsikoudis, Eleftherios; Lee, Edward A., The fixed-point theory of strictly causal functions (Jun 2013), EECS Department, University of California: EECS Department, University of California Berkeley, Technical report UCB/EECS-2013-122
[41] Matsikoudis, Eleftherios; Lee, Edward A., The fixed-point theory of strictly contracting functions on generalized ultrametric semilattices, (Baelde, David; Carayol, Arnaud, Proceedings Workshop on Fixed Points in Computer Science. Proceedings Workshop on Fixed Points in Computer Science, Turino, Italy, September 1st, 2013. Proceedings Workshop on Fixed Points in Computer Science. Proceedings Workshop on Fixed Points in Computer Science, Turino, Italy, September 1st, 2013, Electronic Proceedings in Theoretical Computer Science, vol. 126 (2013), Open Publishing Association), 56-71 · Zbl 1318.68115
[42] Matsikoudis, Eleftherios; Lee, Edward A., On fixed points of strictly causal functions, (Braberman, Víctor; Fribourg, Laurent, Formal Modeling and Analysis of Timed Systems. Formal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 8053 (2013), Springer: Springer Berlin/Heidelberg), 183-197 · Zbl 1318.68114
[43] Matsikoudis, Eleftherios; Stergiou, Christos; Lee, Edward A., On the schedulability of real-time discrete-event systems, (Proceedings of the Eleventh ACM International Conference on Embedded Software. Proceedings of the Eleventh ACM International Conference on Embedded Software, EMSOFT ’13 (2013), IEEE Press), 12:1-12:15 · Zbl 1318.68117
[44] Matthews, Steve G., Partial metric topology, Ann. New York Acad. Sci., 728, 1, 183-197 (1994) · Zbl 0911.54025
[45] Mermin, N. David, Is the moon there when nobody looks? Reality and the quantum theory, Phys. Today, 38, 4, 38-47 (1985)
[46] Milner, Robin; Tofte, Mads, Co-induction in relational semantics, Theoret. Comput. Sci., 87, 1, 209-220 (1991) · Zbl 0755.68100
[47] Moller, Faron; Tofts, Chris, A temporal calculus of communicating systems, (Baeten, J.; Klop, J., CONCUR ’90 Theories of Concurrency: Unification and Extension. CONCUR ’90 Theories of Concurrency: Unification and Extension, Lecture Notes in Computer Science, vol. 458 (1990), Springer: Springer Berlin/Heidelberg), 401-415
[48] Müller, Olaf; Scholz, Peter, Functional specification of real-time and hybrid systems, (Maler, Oded, Hybrid and Real-Time Systems. Hybrid and Real-Time Systems, Lecture Notes in Computer Science, vol. 1201 (1997), Springer: Springer Berlin/Heidelberg), 273-285
[49] Naundorf, Holger, Strictly causal functions have a unique fixed point, Theoret. Comput. Sci., 238, 1-2, 483-488 (2000) · Zbl 0944.68121
[50] Nicollin, Xavier; Sifakis, Joseph; Yovine, Sergio, From ATP to timed graphs and hybrid systems, (de Bakker, J.; Huizing, C.; de Roever, W.; Rozenberg, G., Real-Time: Theory in Practice. Real-Time: Theory in Practice, Lecture Notes in Computer Science, vol. 600 (1992), Springer: Springer Berlin/Heidelberg), 549-572 · Zbl 0790.68067
[51] Oppenheim, Alan V.; Willsky, Alan S.; Nawab, S. Hamid, Signals & Systems (1996), Prentice-Hall
[52] Park, David, Fixpoint induction and proofs of program properties, (Meltzer, B.; Miehie, D., Machine Intelligence, vol. 5 (1969), Edinburgh University Press), 59-78 · Zbl 0219.68007
[53] Pnueli, Amir; Shalev, M., What is in a step: on the semantics of statecharts, (Ito, Takayasu; Meyer, Albert, Theoretical Aspects of Computer Software. Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, vol. 526 (1991), Springer: Springer Berlin/Heidelberg), 244-264 · Zbl 1493.68121
[54] Priess-Crampe, Sibylla; Ribenboim, Paulo, Fixed points, combs and generalized power series, Abh. Math. Semin. Univ. Hambg., 63, 1, 227-244 (1993) · Zbl 0788.06004
[55] Priess-Crampe, Sibylla; Ribenboim, Paulo, Generalized ultrametric spaces I, Abh. Math. Semin. Univ. Hambg., 66, 1, 55-73 (1996) · Zbl 0922.54028
[56] Priess-Crampe, Sibylla; Ribenboim, Paulo, Ultrametric spaces and logic programming, J. Log. Program., 42, 2, 59-70 (2000) · Zbl 0944.68027
[57] Reed, George M.; Roscoe, A. William, A timed model for communicating sequential processes, (Kott, Laurent, Automata, Languages and Programming. Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 226 (1986), Springer: Springer Berlin/Heidelberg), 314-323
[58] Reed, George M.; Roscoe, A. William, Metric spaces as models for real-time concurrency, (Main, M.; Melton, A.; Mislove, M.; Schmidt, D., Mathematical Foundations of Programming Language Semantics. Mathematical Foundations of Programming Language Semantics, Lecture Notes in Computer Science, vol. 298 (1988), Springer: Springer Berlin/Heidelberg), 331-343
[59] Roscoe, A. William, Topology, computer science, and the mathematics of convergence, (Reed, G. M.; Roscoe, A. W.; Wachter, R. F., Topology and Category Theory in Computer Science (1991), Oxford University Press, Inc.: Oxford University Press, Inc. New York, NY, USA), 1-27, Chap. 1 · Zbl 0744.54002
[60] Rounds, William C., Applications of topology to semantics of communicating processes, (Brookes, Stephen; Roscoe, Andrew; Winskel, Glynn, Seminar on Concurrency. Seminar on Concurrency, Lecture Notes in Computer Science, vol. 197 (1985), Springer: Springer Berlin/Heidelberg), 360-372 · Zbl 0565.68022
[61] Sangiorgi, Davide, On the origins of bisimulation and coinduction, ACM Trans. Program. Lang. Syst., 31, 4, 1-41 (2009) · Zbl 1285.68112
[62] Schörner, Erwin, Ultrametric fixed point theorems and applications, (Valuation Theory and Its Applications. Valuation Theory and Its Applications, Fields Institute Communications, vol. II (2003), American Mathematical Society), 353-359 · Zbl 1036.54015
[63] Scott, Dana S.; de Bakker, Jaco W., A theory of programs (1969), IBM Research Center: IBM Research Center Vienna, Austria, Unpublished notes, Seminar on Programming
[64] Tarski, Alfred, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 2, 285-309 (1955) · Zbl 0064.26004
[65] Yates, Robert, Networks of real-time processes, (Best, Eike, CONCUR’93. CONCUR’93, Lecture Notes in Computer Science, vol. 715 (1993), Springer: Springer Berlin/Heidelberg), 384-397
[66] Yates, Robert; Gao, Guang, A Kahn principle for networks of nonmonotonic real-time processes, (Bode, Arndt; Reeve, Mike; Wolf, Gottfried, PARLE ’93 Parallel Architectures and Languages Europe. PARLE ’93 Parallel Architectures and Languages Europe, Lecture Notes in Computer Science, vol. 694 (1993), Springer: Springer Berlin/Heidelberg), 209-227
[67] Yi, Wang, CCS + time = an interleaving model for real time systems, (Albert, Javier; Monien, Burkhard; Artalejo, Mario, Automata, Languages and Programming. Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 510 (1991), Springer: Springer Berlin/Heidelberg), 217-228 · Zbl 0769.68027
[68] Zeigler, Bernard P., Theory of Modeling and Simulation (1976), John Wiley & Sons · Zbl 0352.68122
[69] Zeigler, Bernard P.; Praehofer, Herbert; Kim, Tag Gon, Theory of Modeling and Simulation (2000), Academic Press
[70] Zhao, Yang; Liu, Jie; Lee, Edward A., A programming model for time-synchronized distributed real-time systems, (Real Time and Embedded Technology and Applications Symposium. Real Time and Embedded Technology and Applications Symposium, 13th IEEE 2007, RTAS ’07 (April 2007)), 259-268
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.