Abstract
We extend Lamport's partial-ordering models[10] for real-time computing and invent to use the concept of named transactions to reference groups of related events. We then propose Transaction Partial-Ordering Logic (TPOL) as a new specification language with special syntax and high-level semantics tailored to describe the interaction among transactions in a distributed real-time system. Finally we examine TPOL satisfiability problems with different restrictions.
Supported by NSC, Taiwan, ROC under grant NSC 84-2213-E-001-012.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur and T.A. Henzinger, A really temporal logic, in Pro. 30th IEEE Symp. Found. of Computer Sciences, pp. 164–169, 1989.
E.M. Clarke, E.A. Emerson, Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic, Proceedings of Workshop on Logics of Programs, Lecture Notes in Computer Science, Vol. 131 (Springer-Verlag, Berlin, 1981) pp. 52–71.
E. 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), 1986, pp. 244–263.
R.W. Floyd, New Proofs and Old Theorems in Logic and Formal Linguistics, Computer Associates Inc., Wakefield, Mass.
J.E. Hopcroft, J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979.
F. Jahanian and A.K. Mok, Safty analysis of timing properties in realtime systems, IEEE Transactions on Software Engineering, SE-12(9):890–904, September 1986.
F. Jahanian and A.K. Mok, A graph theoretic approach for timing analysis and its implementation, ACM Transactions on Computers, C-36(12):961–975, August 1987.
F. Jahanian and A.K. Mok, Modechart: a Specification Language for Real-Time Systems, IEEE Transactions on Software Engineering, 1988.
C.B. Jones, A pi-calculus Semantics for an Object-Based Design Notation, 1993 CONCUR.
L. Lamport, Time, Clocks, and the Ordering of Events in a Distributed Systems, Communication of the ACM, July 1978, Vol. 21, Number 7, pp. 558–565.
L. Lamport, Sometimes is Sometimes “Not Never”-on the temporal logic of programs, 7th Annual ACM Symp. on Principles of Programming Languages, 1980, pp. 174–185.
A. Pnueli, The Temporal Logic of Programs, 18th annual IEEE-CS Symp. on Foundations of Computer Science, pp. 45–57, 1977.
E. Post, A Variant of a Recursively Unsolvable Problem, Bull, AMS, 52, 264–268.
A. Silberschatz, J.L. Peterson, Operating System Concepts, Alternate Edition, Addison-Wesley, 1988.
J.A. Stankovic, A Serious Problem for Next-Generation Systems, IEEE Computer, October, 1988, pp 10–19.
F. Wang, A. Mok, E.A. Emerson, Distributed Real-Time System Specification and Verification in APTL, ACM Transaction on Software Engineering and Methodology, Oct, 1993.
F. Wang and A.K. Mok, Asynchronous real-time event logic, Proceedings of International Computer Symposium, Taiwan, 1992.
F. Wang and A.K. Mok, RTL and Refutation by Positive Cycles, to appear in Proceedings of Formal Method Europe Symposium, Spain, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, F. (1995). A temporal logic for real-time partial-ordering with named transactions. In: Baeza-Yates, R., Goles, E., Poblete, P.V. (eds) LATIN '95: Theoretical Informatics. LATIN 1995. Lecture Notes in Computer Science, vol 911. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59175-3_113
Download citation
DOI: https://doi.org/10.1007/3-540-59175-3_113
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59175-7
Online ISBN: 978-3-540-49220-7
eBook Packages: Springer Book Archive