Nonstandard Dynamic Logic Papers of AN

First order Dynamic Logic (as opposed to Propositional DL) with standard semantics is rather wild, it cannot have a decidable proof system, even if we select an acceptably small sublanguage of it, see ANBSL78, ANSMFCS79. The reason for this is that standard semantics assumes processes to run in standard time, i.e., along the natural numbers. If we make dependence on time explicit so that we can ``talk” about processes living in time, we get a Dynamic Logic with explicit time semantics, or in other words, with nonstandard time semantics. Let’s call the resulting logic Nonstandard Dynamic Logic (NDL). In NDL we are not tied to the natural numbers as the only possible time structure, and we can make explicit requirements (i.e., axioms) about the time structure. As a consequence of explicitness, NDL has a decidable and complete proof system, see ANSTCS82.

NDL provides an adequate background (or frame) logic for talking about programs, processes, actions. In NDL we can express partial and total correctness as well as many other properties of programs like concurrency, nondeterminism, fairness. NDL has been used for characterizing the “information contents” of distinguished well known program verification methods, for comparing powers of program verification methods as well as for generating new ones. [NKoz82, ANSTCS82, ASalw83]

List of papers

Completeness of Floyd logic. Bulletin of the Section of Logic, 7/3 (1978), 115-120. Andreka, H., Nemeti, I. pdf [ANBSL78] Abstract

Program verification within and without logic. Bulletin of the Section of Logic, 8/3 (1979), 124-129. Andreka, H., Nemeti, I., Sain, I. pdf [ANSBSL79] Abstract

Henkin-type semantics for program schemes to turn negative results to positive. In: Fundamentals of Computation Theory'79 (Proc. Conf. Berlin 1979) Ed.: L. Budach, Akademie-Verlag, Berlin, 1979. Band 2, 18-24. Andreka, H. , Nemeti, I. , Sain, I. pdf [ANSFCT79]

Completeness problems in verification of programs and program schemes. In: Mathematical Foundations of Computer Science'79 (Proc. Conf. Olomouc Czechoslovakia 1979), Lecture Notes in Computer Science Vol 74, Springer-Verlag, Berlin, 1979, 208-218. Andreka, H., Nemeti, I., Sain, I. pdf [ANSMFCS79] Abstract

A characterization of Floyd provable programs. In: Mathematical Foundations of Computer Science'81 (Proc. Conf. Strbské Pleso, Czechoslovakia 1981). Eds.: Gruska,J. Chytil,M. Lecture Notes in Computer Science Vol 118, Springer-Verlag, Berlin, 1981, 162-171.

Andreka, H., Nemeti, I., Sain, I. pdf [ANSMFCS81] Abstract

Nonstandard dynamic logic (Invited paper.) In: Logics of Programs (Proc. Conf. New York, May 1981) Ed.: Kozen,D. Lecture Notes in Computer Science Vol 131, Springer-Verlag, Berlin, 1982 311—348. Nemeti, I. pdf [NKoz82] Abstract

A complete logic for reasoning about programs via nonstandard model theory. Theoretical Computer Science 17 1982. Part I in No 2, pp.193-212, Part II in No 3, pp.259-278. Andreka, H., Nemeti, I., Sain,I. Part I pdf Part II pdf [ANSTCS82] Abstract

Sharpening the characterization of the power of Floyd method. In: Logics of Programs and their Applications (Proc. Conf. Poznan 1980) Ed.: Salwicki,A. Lecture Notes in Computer Science Vol 148, Springer-Verlag, Berlin, 1983, 1-26. Andreka, H. pdf [ASalw83] Abstract

Nonstandard runs of Floyd-provable programs. In: Logics of Programs and their Applications (Proc. Conf. Poznan 1980) Ed.: Salwicki, A. Lecture Notes in Computer Science Vol 148, Springer-Verlag, Berlin, 1983 186-204. Nemeti, I. pdf [NSalw83] Abstract

On the strength of temporal proofs. In: Mathematical Foundations of Computer Science'89 (Proc. Porabka-Kozubnik, Poland, 1989) Eds.: Kreczmar,A. Mirkowska,G. Lecture Notes in Computer Science Vol 379, Springer-Verlag, Berlin, 1989, 135-144. Andreka, H., Nemeti, I., Sain, I. pdf [ANSMFCS89]

On the strength of temporal proofs. Theoretical Computer Science 80 1991, 125-151. Shorter version appeared in Lecture Notes in Computer Science Vol 379, 1989. Andreka, H., Nemeti, I., Sain, I. pdf available from authors [ANSTCS91]

Effective temporal logics of programs. In: Time and Logic, a computational approach, eds: Bolc,L. and Szalas,A., UCL Press, London, 1995. pp.51-129. Andreka, H. Goranko,V. Mikulas,Sz. Nemeti,I. and Sain,I. pdf available from authors [AGorMNS95]

Preprints

A characterisation of Floyd-provable programs. MKI Preprint No 8/1978, February 1978. 27pp. Andreka, H., Nemeti, I., pdf available from authors

Classical many-sorted model theory to turn negative results on program schemes to positive. Preprint Math. Inst. H.A.S., 1979. Andreka, H., Nemeti, I. pdf available from authors

A complete first order dynamic logic. Preprint, Mathematical Institute of Hungarian Academy of Sciences, 1979. Version 810930. 124 pp. Andreka, H., Nemeti, I., Sain, I. pdf [ANSComp81] Abstract