Abstract
The situation calculus (SC) is a formalism for reasoning about action. Within SC, the notion of state of a given situation is usually characterized by the set of fluents that hold in that situation. However, this concept is insufficient for system specification. To overcome this limitation, an extension of SC is proposed, the situation and state calculus (SSC), where the concept of state is primitive, just like actions, situations and fluents. SSC is then compared with a branching temporal logic (BTL). A representation of BTL in SSC is defined and shown to establish a sound and complete encoding.
★
We would like to thank our colleagues in the ASPIRE project, and also to Alberto Zanardo, Cristina Sernadas and Javier Pinto their valuable comments and suggestions at some stages of this work. This work was partially supported by FCT, the PRAXIS XXI Projects 2/2.1/MAT/262/94 SitCalc, PCEX/P/MAT/46/96 ACL, 2/2.1/TIT/1658/95 LogComp, the ProbLog initiative of CMA, as well as the ESPRIT IV Working Groups 22704 ASPIRE and 23531 FIREworks.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J. P. Burgess. Logic and time. Journal of Symbolic Logic, 44:566–582, 1979.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, New York, N.Y., 1985.
J. Fiadeiro and A. Sernadas. Structuring theories on consequence. In D. Sannella and A. Tarlecki, editors, Proceedings of the 5th Workshop on Recent Trends in Data Type Specification, volume 332 of LNCS, pages 44–72, Berlin, 1988. Springer.
M. Gelfond, V. Lifschitz, and A. Rabinov. What are the limitations of the situation calculus? In Robert Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, pages 167–179. Kluwer Academic, Dordrecht, 1991.
J. Goguen and R. M. Burstall. Introducing institutions. In E. Clarke and D. Kozen, editors, Logics of Programs: Workshop, Carnegie Mellon University, June 1983, volume 164 of LNCS, pages 221–256. Springer-Verlag, New York, N.Y., 1984.
V. Lifschitz and A. Rabinov. Miracles in formal theories of action. Articial Intelligence, 38:225–237, 1989.
Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 93:97–130, 1991.
J. McCarthy and P. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 463–502. Edinburgh University Press, Scotland, 1969.
J. Meseguer. General logics. In H.-D. Ebbinghaus et al, editor, Proc. Logic Colloquium’ 87. North-Holland, 1989.
R. Miller and M. Shanahan. Narratives in the situation calculus. Journal of Logic and Computation — Special Issue on Actions and Processes, 4(5):513–530, 1994.
J. Pinto and R. Reiter. Reasoning about time in the situation calculus. Annals of Mathematics and Artificial Intelligence: Papers in Honour of Jack Minker, 14(2–4):251–268, 1995.
J. Ramos. The situation and state calculus. In A. Drewery, G.-J. Kruijff and R. Zuber, editors, Proceedings of the Second ESSLLI Student Session, 1997.
R. Reiter. The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 359–380. Academic Press, San Diego, CA, 1991.
R. Reiter. Proving properties of states in the situation calculus. Articial Intelligence, 64:337–351, 1993.
A. Sernadas, C. Sernadas, and J. Costa. Object specification logic. Journal of Logic and Computation, 1:7–25, 1995.
A. Sernadas, C. Sernadas, and J. Ramos. A temporal logic approach to object certification. Data and Knowledge Engineering, 19:267–294, 1996.
C. Stirling. Modal and temporal logics. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science. Volume 2. Background: Computational Structures, pages 477–563. Oxford University Press, 1992.
J. van Benthem. Correspondence theory. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, volume 165 of Synthese Library, chapter II.4, pages 167–247. D. Reidel Publ. Co., Dordrecht, 1984.
A. Zanardo. Branching-time logic with quantification over branches: The point of view of modal logic. Journal of Symbolic Logic, 61(1):1–39, 1996.
A. Zanardo, B. Barcellan, and M. Reynolds. Non-denability of the class of complete bundled trees. The Logic Journal of IGPL. To appear.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ramos, J., Sernadas, A. (1999). The Situation and State Calculus versus Branching Temporal Logic. In: Fiadeiro, J.L. (eds) Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, vol 1589. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48483-3_19
Download citation
DOI: https://doi.org/10.1007/3-540-48483-3_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66246-4
Online ISBN: 978-3-540-48483-7
eBook Packages: Springer Book Archive