Abstract
Future Interval Logic (FIL) is a linear-time temporal logic that is intended for specification and verification of reactive and concurrent systems. To make FIL useful for specifying and reasoning about practical systems, we present a first-order extension of FIL, including equality and n-ary function and predicate symbols, and a set of sound proof rules for reasoning in the logic. We illustrate the use of the logic by specifying a sliding window protocol and proving that the specifications satisfy a set of correctness requirements.
This research was supported in part by NSF/ARPA grant CCR-9014382.
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., “The power of temporal proofs,” Theoretical Computer Science, vol. 65, no. 1, pp. 35–83, June 1989.
Abadi, M. and Manna, Z., “Non-clausal deduction in first-order temporal logic,” Journal of the ACM, vol. 37, no. 2, pp. 279–317, April 1990.
Cardell-Oliver, R., “The specification and verification of sliding window protocols in higher order logic,” Technical Report No. 183, Computer Laboratory, University of Cambridge, October 1989.
Dillon, L. K., Kutty, G., Moser, L. E., Melliar-Smith, P. M., Ramakrishna, Y. S., “Graphical specifications for concurrent software systems,” Proceedings of the 14th International Conference on Software Engineering, Melbourne, Australia, pp. 214–224, May 1992.
Garson, J. W., “Quantification in modal logic,” in Handbook of Philosophical Logic, Gabbay, D. and Guenthner, F. (eds.), vol. II, pp. 249–307, D. Reider Publishing Co., 1984.
Kutty, G., Ramakrishna, Y. S., Moser, L. E., Dillon, L. K., Melliar-Smith, P. M., “A Graphical Interval Logic toolset for verifying concurrent systems,” Proceedings of the 5th Conference on Computer Aided Verification, Elounda, Crete, Greece, Lecture Notes in Computer Science 697, Springer Verlag, pp. 138–153, June 1993.
Kutty, G., Moser, L. E., Melliar-Smith, P. M., Ramakrishna, Y. S., Dillon, L. K., “Axiomatizations of interval logics,” to appear in Fundamenta Informaticae.
Koymans, R., “Specifying message passing systems requires extending temporal logic,” Proceedings of the Colloquium on Temporal Logic in Specification, Lecture Notes in Computer Science 398, pp. 213–223, Springer-Verlag, 1989.
Manna, Z. and Pnueli, A., “Verification of concurrent programs: A temporal proof system,” Foundations of Computer Science IV: Distributed Systems, Mathematical Centre Tracts, 159, Amsterdam, pp. 163–255, 1983.
Manna, Z. and Pnueli, A., The temporal logic of reactive and concurrent systems, Springer-Verlag, New York, Inc., 1992.
Paliwoda, K. and Sanders, J. W., “An incremental specification of the sliding window protocol,” Distributed Computing, no. 5, pp. 83–94, 1991.
Ramakrishna, Y. S., Dillon, L. K., Moser, L. E., Melliar-Smith P. M., Kutty, G., “An automata-theoretic decision procedure for future interval logic,” Proceedings of the Twelfth Conference on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, Lecture Notes in Computer Science 652, Springer-Verlag, pp. 51–67, December 1992.
Richier, J. L., Rodriguez, C, Sifakis, J. and Voiron, J.,“Verification in Xesar of the sliding window protocol,” Proceedings of the IFIP WG 6.1 7th International Conference on Protocol Specification, Testing and Verification, Zurich, Switzerland, pp. 235–248, May 1987.
Schwartz, R. L., Melliar-Smith, P. M. and Vogt, F., “An interval based temporal logic,” Proceedings of the ACM Workshop on the Logics of Programming, pp. 443–457, June 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kutty, G., Moser, L.E., Melliar-Smith, P.M., Dillon, L.K., Ramakrishna, Y.S. (1994). First-order future interval logic. In: Gabbay, D.M., Ohlbach, H.J. (eds) Temporal Logic. ICTL 1994. Lecture Notes in Computer Science, vol 827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013989
Download citation
DOI: https://doi.org/10.1007/BFb0013989
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58241-0
Online ISBN: 978-3-540-48585-8
eBook Packages: Springer Book Archive