Logika temporalna w informatyce

Kazimierz Trzęsicki

Kazimierz Trzęsicki Uniwersytet w Białymstoku

Słowa kluczowe: logika, informatyka, logika temporalna, weryfikowanie systemów informatycznych

Abstrakt

Leibniz intended to create a lingua characteristica universalis, a language, in which all knowledge (expressiveness) could be recorded, and a calculus ratiocinator, a method that would make it possible to define in a calculational manner the truth of any sentence in this language. Such an idea is at the basis of contemporary logic. With respect to the correctness of the equipment and of programs such an idea is at the foundations of logical methods of verification of software systems.

Today we can see that a further development of informatics indeed depends on the progress of research in logic, and logic – this ancient discipline – has found a rich field for investigations; it has gained new perspectives for studies. Its applications may have a significant practical dimension that philosophers have never dreamed about.

Bibliografia

Allen J. F. 1985: Charles Hamblin (1922–1985), „The Australian Computer Journal” s. 194-195.

Baier C., Katoen J.-P. 2008: Principles of Model Checking, Foreword by Kim Guldstrand Larsen, The MIT Press.

Barton R.S. 1970: Ideas for computer systems organization: a personal survey, [w:] J. S. Jou (ed.), ‘Software Engineering’. Proceedings of the Third Symposium on Computer and Information Sciences held in Miami Beach, Florida, December 1969, Vol. 1, New York, NY: Academic Press, s. 7-16.

Boehm B. W. 1981: Software Engineering Economics, Prentice-Hall.

Bradfield J.C., Stirling C. 2001: Modal logics and μ-calculi: An introduction, [w:] J.A. Bergstra, A. Ponse, S.A. Smolka (eds), Handbook of Process Algebra, Elsevier Science, chapter 4, s. 293-330.

Chaitin G.J. 2004: Wissen und glauben/knowledge and belief, [w:] W. Löffler, P. Weingartner (eds), Akten des 26. Internationalen Wittgenstein-Symposiums 2003, Wien: ÖBV & HPT, s. 277-286.

Clarke E.M. 2008: The birth of model checking, [w:] DBLP:conf/spin/5000, s. 1-26.

Clarke E.M., Emerson E.A. 1982: Design and synthesis of synchronization skeletons using branching-time temporal logic, [w:] Logic of Programs, Workshop, (Lecture Notes in Computer Science, Vol. 131), London, UK: Springer-Verlag, s. 52-71.

Clarke E.M., Emerson E.A., Sistla A.P. 1986: Automatic verification of finite-state concurrent systems using temporal logic specifications, „ACM Transactions on Programming Languages and Systems” (2), s. 244-263.

Coe T., Mathisen T., Moler C., Pratt V. 1995: Computational aspects of the pentium affair, „ IEEE Computational Science & Engineering” vol. 2, 1, s. 18-31.

Daskalopulu A. 2000: Model checking contractual protocols, [w:] J. Breuker, R. Leenes, R. Winkels (eds), ‘Legal Knowledge and Information Systems’, JURIX 2000: The 13th Annual Conference, IOS Press, Amsterdam, pp. 35–47.

Davis M. 1988: Influences of mathematical logic on computer science, [w:] A half-century survey on The Universal Turing Machine, New York, NY: Oxford University Press, s. 315-326.

Davis M. 2000: The Universal Computer: The Road from Leibniz to Turing, New York: W.W. Norton & Company.

Dijkstra E.W. 1968: Notes on structured programming, [w:] E.W.D.O.-J. Dahl, C.A.R. Hoare (eds), Structured Programming, London: Academic Press, s. 1-82.

Dijkstra E.W. 1989: In reply to comments. EWD1058.

Emerson E. A. 2008: The beginning of model checking: A personal perspective, [w:] DBLP:conf/spin/5000, s. 27-45.

Giunchiglia F., Traverso P. 1999: Planning as model checking, [w:] Proceedings of the Fifth European Workshop on Planning, (ECP’99), Springer, s. 1-20.

Grumberg O., Veith H. (eds) 2008: Years of Model Checking – History, Achievements, Perspectives, (Lecture Notes in Computer Science, Vol. 5000), Springer.

Hamblin C. L. 1970: Fallacies, London: Methuen.

Hamblin C. L. 1987: Imperatives, Oxford: Basil Blackwell.

Heath J., Kwiatowska M., Norman G., Parker D., Tymchysyn O. 2006: Probabalistic model checking of complex biological pathways, [w:] C. Priami (ed.), Proc. Comp. Methods in Systems Biology, (CSMB’06), (Lecture Notes in Bioinformatics, Vol. 4210), Springer, s. 32-47.

Hoare T. 2003: The verifying compiler: A grand challenge for computing research, „Journal of the ACM” vol. 50, 1, s. 63-69.

Kaufmann M., Moore J.S. 2004: Some key research problems in automated theorem proving for hardware and software verification, „Revista de la Real Academia de Ciencias (RACSAM)”. Serie A, 98 (1), s. 181-196.

Kautz H., Selman B. 1992: Planning as satisfiability, [w:] ECAI ’92: Proceedings of the 10th European conference on Artificial intelligence, New York, NY: John Wiley & Sons, s. 359–363.

Künzel W. 2006: The birth of the machine: Raymundus Lullus and his invention, http://www.c3.hu/scca/butterfly/Kunzel/synopsis.html

Leibniz G.W. 1685: Machina arithmetica in qua non additio tantum et subtractio sed et multiplicatio nullo, divisio vero paene nullo animi labore peragantur, Vol. Math. III A.2-c.

Leibniz G.W. 1697: Brief an den Herzog von Braunschweig-Wolfenbüttel Rudolph August, 2. Januar 1697’, http://www.fhaugsburg.de/ harsch/germanica/Chronologie/17Jh/ Leibniz/ lei_-bina.html

Leibniz G.W. 1890: Philosophische Schriften, Vol. VII, Berlin.

Leibniz G.W. 2006: Sämtliche Schriften und Briefe, (Zweite Reihe Philosophischer Briefwechsel, Vol. 1), Akademie Verlag.

Manna Z., Pnueli A. 1992, 1995: The Temporal Logic of Reactive and Concurrent Systems, Vol. 1: Specification, 2: Safety, New York.

Pnueli A. 1977: The temporal logic of programs, [w:] Proceedings of the 18th IEEE-CS Symposium on Foundation of Computer Science (FOCS-77), IEEE Computer Society Press, s. 46-57.

Pnueli A. 1981: The temporal semantics of concurrent programs, „Theoretical Computer Science” vol. 13, s. 45-60.

Pratt V.R. 1980: Applications of modal logic to programming, „Studia Logica”, s. 257-274.

Prior A.N. 1967: Past, Present and Future, Oxford University Press.

Prior A.N. 1996: A statement of temporal realism, [w:] B.J. Copeland (ed.), Logic and Reality: Essays on the Legacy of Arthur Prior, Oxford University Press.

Queille J.-P., Sifakis J. 1982: Specification and verification of concurrent systems in CESAR, [w:] Proceedings 5th International Symposium on Programming, (Lecture Notes in Computer Science, Vol. 137), Springer-Verlag, s. 337-351.

Quine W.V.O. 1966: On the application of modern logic, [w:] The Ways of Paradox and Other Essays, New York: Random House, s. 35–41.

Rescher N. Urquhart A. 1971, Temporal Logic, Wien–New York: Springer.

Schnoebelen P. 2002: The complexity of temporal logic model checking, „Advances in Modal Logic”, s. 1-44.

Trzęsicki K. 2005: Arthura Normana Priora związki ze szkołą lwowsko-warszawską, [w:] K. Trzęsicki (red.), Ratione et studio, Białystok: Uniwersytet w Białymstoku, s. 269-288.

Trzęsicki K. 2006a: From the idea of decidability to the number Ω, „Studies in Grammar, Logic and Rethoric” (22), s. 73-142.

Trzęsicki K. 2006b: Leibniza idea systemu binarnego, [w:] J. Kopania, H. Święczkowska (red.), Filozofia i myśl społeczna XVII w., Białystok, s. 183-203.

Trzęsicki K. 2006c: Leibnizjańskie inspiracje informatyki, „Filozofia Nauki” (3), s. 21-48.

Turing A.M. 1936-1937: On computable numbers, with an application to the Entscheidungsproblem, „Proceedings of the London Mathematical Society” (Series 2), s. 230-265. Received May 25, 1936; Appendix dodany 28 sierpnia; read November 12, 1936; corrections ibid. vol. 43 (1937), s. 544-546. Artykuł Turinga ukazał się w Part 2 vol. 42, wydanym w grudniu 1936 (Przedruk w: M. Davis (ed.) 1965, s. 116-151; corr. ibid. pp. 151–154). Online: http://www.abelard.org/turpap2/tp2-ie.asp

Turing A.M. 1986: Lecture to the London Mathematical Society on 20 February 1947, [w:] B. Carpenter, R. Doran (eds), A. M. Turing’s ACE Report of 1946 and Other Papers, Cambridge, Mass.: MIT Press.

Wang W., Hidvegi Z., Bailey A., Whinston A. 2000: E-process design and assurance using model checking, „IEEE Computer” (10), s. 48-53.