Eng During last 365 days Approved articles: 2088,   Articles in work: 308 Declined articles: 853 
Articles and journals | Tariffs | Payments | Your profile

Back to contents

Mosaic method for the logics of time
Tolstukhin Aleksei

Post-graduate student, the department of Logics, M. V. Lomonosov Moscow State University

119234, Russia, Moskva oblast', g. Moscow, ul. Leninskie Gory, 1, of. 834





The subject of this research is logics with the linear flow of time. Currently, such system are represent interest not only from the philosophical perspective, but also have practical application in the field of informatics. For both of the indicated areas of knowledge, relevant is the question of proof of formulas in the system, in other words, presents of the decision procedure. Since the early XXI century, one of the approaches towards the problem of decidability of the temporal logics is the procedure of recursive structuring of the model for a formula, which is realizes in accordance with the mosaic principle, small fragments of large model that manifest as “construction” elements” of a supposedly infinite model. The work conducts a detailed analysis of the recent case studies dedicated to this problematic, as well as their systematization. The author is the first to perform a detailed analysis in the Russian language. The article presents not only the idea of mosaic method, but also demonstrates the key lemmas proving the effectiveness of this approach. The next step can be considered the development of calculation based on the mosaic method, proof of its consistency and completeness.

Keywords: decision procedure, linear, flow of time, defects of temporal structure, mosaics, modal logic, temporal logic, Mosaic Method, satisfability, saturated set of mosaics



Article was received:


Review date:


Publish date:


This article written in Russian. You can find full text of article in Russian here .

Barringer H., Kuiper R., and Pnueli A. A really abstract concurrent model and its temporal logic. // Proceedings of the 13th ACM symposium on the principles of Programming Languages. St. Petersberg Beach, Florida. ACM, January 1986.
Bian J., French T. and Reynolds M. An Efficient Tableau for Linear Time Temporal Logic. // Stephen Cranefield and Abhaya Nayak, editors, 26th Australasian Joint Conference on Artificial Intelligence, AI 2013. 1-6 December 2013, Dunedin, New Zealand. 2013. V. 8272. P. 289300.
Burgess J.P. Axioms for tense logic I: Since and Until.// Notre Dame Journal of Formal Logic. 1982. V. 23 No 2. P. 367-374.
Burgess J.P. and Gurevich Y. The decision problem for linear temporal logic. // Notre Dame Journal of Formal Logic. 1985. V. 26 No 2. P. 115-128.
Kamp H. Tense Logic and the Theory of Linear Order. PhD thesis. University of California, Los Angeles. 1968.
Marx M., Mikulás S., and Reynolds M. The mosaic method for temporal logics. // Dyckhoff R., editor, Automated Reasoning with Analytic Tableaux and Related Methods. Proceeding of International Conference TABLEAUX-2000. LNAI 1847. Springer, 2000. P. 324-340.
Marx M. Venema Y. A modal logic of relations. // E. Orlowska, editor, Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa. Phesica-Verlag, Heidelberg/New York. P. 124-167.
Németi I. Free Algebras and Decidability in Algebraic Logic. PhD thesis. Hungarian Academy of Sciences, Budapest. 1986.
Németi I. Decidable versions of first order logic and cylindric-relativized set algebras. // Csirmaz L., Gabbay D.M., and de Rijke M., editors, Logic Colloquium 92. CSLI Publications. 1995. P. 171-241.
Pnueli A. The temporal logic of programs. // In Proceedings of the Eighteenth Symposium on Foundations of Computer Science. Providence, RI. 1977. P. 46-57.
Reynolds M. A decidable logic of parallelism. // Notre Dame Journal of Formal Logic. 1997. V. 38. P. 419-436.
Reynolds M. Dense time reasoning via mosaics. // In Carsten Lutz, Jean-François Raskin, editor, TIME 09: Proceedings of the 2009 16th International Symposium on Temporal Representation and Reasoning, 2009. P. 310.
Reynolds M. Tableau for general linear temporal logic. // Journal of Logic and Computation. 2013. V. 23 (5). P. 10571080.
Reynolds M. The complexity of temporal logic over the reals.// Annals of Pure and Applied Logic. 2010. V. 161 (8). P. 1063-1096.
Reynolds M. The complexity of the temporal logic with "until" over linear time. // Journal of Computer and System Sciences. 2003. V. 66 (2). P. 393-426.
Grigor'ev O. M. Analitiko-tablichnaya formalizatsiya sistem vremennoi logiki. Kandidatskaya dissertatsiya. Moskva. 2004.