Abstract
The paper presents a method for formally proving correctness of processes specified by transition systems which is based on a tableau calculus for an extended temporal logic. The model-theoretic semantics is given by labeled Kripke structures, incorporating information about the actions performed in transitions. Extending first-order CTL for handling action labels, the multi-modal logic MCTL is defined which is well-suited for specifying transition systems and their properties. For MCTL, a tableau semantics and -calulus is presented, allowing formal verification.
Supported by grant no. GRK 184/1-97 of the Deutsche Forschungsgemeinschaft.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Ben-Ari, Z. Manna, and A. Pnueli. The Temporal Logic of Branching Time. In 8th ACM Symp. on Principles of Programming Languages, 1981.
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.
R. DeNicola and F. Vaandrager. Action versus State Based Logics for Transition Systems. In Semantics of Systems of Concurrent Processes, Springer LNCS 469, pp. 407–419, 1990.
E. A. Emerson and J. Y. Halpern. “Sometimes” and “not never” revisited: On Branching Time versus Linear Time in Temporal Logic. In 10th ACM Symp. on Principles of Programming Languages, 1983.
M. Fitting. First Order Logic and Automated Theorem Proving. Springer, New York, 1990.
D. Harel. First-Order Dynamic Logic, volume 68 of LNCS. Springer, 1979.
M. Hennessy and R. Milner. Algebraic Laws for Non-determinism and Concurrency. Journal of the ACM, 32:137–161, 1985.
R. Milner. Operational and Algebraic Semantics of Concurrent Processes, Ch. 19, pp. 1201–1242 of Handbook of Theoretical Computer Science, J. v. Leeuwen, ed., Volume B: Formal Models and Semantics, Elsevier, 1990.
W. May and P. H. Schmitt. A Tableau Calculus For First-Order Branching Time Logic. Intl. Conf. on Formal and Applied Practical Reasoning, FAPR'96, Springer LNCS 1085, pp. 399–413, 1996.
P. Wolper. The Tableau Method for Temporal Logic. Logique et Analyse, 28:110–111, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
May, W. (1997). Proving correctness of labeled transition systems by semantic tableaux. In: Galmiche, D. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1997. Lecture Notes in Computer Science, vol 1227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027419
Download citation
DOI: https://doi.org/10.1007/BFb0027419
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62920-7
Online ISBN: 978-3-540-69046-7
eBook Packages: Springer Book Archive