On the Computational Power of Querying the History

• Autorzy: Lisitsa A. , Potapov I.
• Języki publikacji: EN

Abstrakty

EN

Querying its own history is an important mechanism in the computations, especially those interacting with people or other computations such as transaction processing, electronic data interchange. John McCarthy in his Elephant programming language proposal suggested exploiting the referring to the past as the main programming primitive. In this paper we study the computational power of such primitive. In order to do that we propose a refined formal model, History Dependent Machine (HDM), which uses querying the history as its sole computational primitive. Our main result may be spelled in general terms as: a model with a single agent wandering around a pool of resources and having ability to check its own history for simple temporal properties has a universal computational power. Moreover, HDM can simulate any multicounter machine in real time. Then we show that the computations of HDM may be specified in the extension of propositional linear temporal logic by flexible constants, the abstraction operator and equality. We use then universality of HDM model to show that the above extension with a single flexible constant is not recursively axiomatizable.

Słowa kluczowe

EN

history-dependent computations; executable temporal logic; models of computations; universality

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 91, nr 2
• Strony: 395--409
• Opis fizyczny: Bibliogr. 14 poz., tab., wykr.

Twórcy

autor

Lisitsa A.

autor

Potapov I.

• Computer Science Department, University of Liverpool Ashton Building, Ashton Street Liverpool, L69 3BX, UK,

Bibliografia

• [1] Jiannong Cao, Xinyu, Feng, Jian Lu, Sajal K. Das, Mailbox-Based Scheme for Mobile Agent Communications, IEEE Computer, Vol. 35, No. 9, September 2002, 54-60.
• [2] H. Barringer, M.Fisher, D. Gabbay, R.Owens, M.Reynolds (eds.), The Imperative Future: Principles of Executable Temporal Logic, Research Studies Press Ltd, 1996.
• [3] V. Blondel, J. Cassaigne, C. Nichitiu, On the Presence of Periodic Configurations in Turing Machines and in Counter Machines, Theoretical Computer Science, 289, (2002), 573-590.
• [4] Jan Chomicki, Damian Niwi´nski, On the Feasibility Checking Temporal Integrity Constraints, Journal of Computer and System Sciences, 51(3), pp 523-535, 1995.
• [5] H. Comon and Y.Jurski, Multiple counters automata, safety analysis and Presburger arithmetic, Research Report LSV-98-1,Mar.1998, Laboratoire Specification at Verification.
• [6] Stéphane Demri, Ranco Lazić, David Nowak, On freeze quantifier in Constraint LTL: decidablity and complexity, 12th International Symposium on Temporal Representation and Reasoning, TIME'05, 113-121, IEEE Computer Society, 2005.
• [7] M. Fitting,Modal Logic Between Propositional and First Order, Journal of Logic and Computation, 12, 1017-1026, 2002.
• [8] Dov M.Gabbay,Mark A. Reynolds,Marcelo Finger, Temporal Logic.Mathematical Foundations and Computational Aspects, Volume 2, Oxford Science Publications, Clarendon Press, 2000.
• [9] Alexei Lisitsa and Igor Potapov, Temporal logic with predicate abstraction, CoRR cs.LO/0410072, The Computing Research Repository, http://xxx.lanl.gov/archive/cs/, 14pp, 2004.
• [10] Alexei Lisitsa and Igor Potapov. Temporal logic with predicate lambda-abstraction, 12th International Symposium on Temporal Representation and Reasoning, TIME'05, 147-155, IEEE Computer Society, 2005.
• [11] John McCarthy. Elephant 2000. Technical report, Stanford Formal Reasoning Group, 1996. Available only as http://www-formal.stanford.edu/jmc/elephant.html.
• [12] M.Minsky, Recursive unsolvability of Post's problem of "tag" and other topics in theory of Turing machines, Annals of Mathematics, 74, pp 437-455, 1961.
• [13] M. Minsky, Computation: Finite and Infinite Machines, Prentice-Hall International, 1967.
• [14] A. Sistla, O. Wolfson, Temporal Triggers in Active Databases, IEEE Transactions on Knowledge and Data Engineering, 7 (3), pp 471-486, 1995.