Abstract
We investigate the hybrid extension of CaRet, denoted HyCaRet, obtained by adding the standard existential binder operator ∃. We show that the one variable fragment 1-HyCaRet of HyCaRet is expressively complete for the first-order logic FO μ which extends FO over words with a binary matching predicate. While all the known FO μ -complete and elementary extensions of CaRet can be linearly translated in 1-HyCaRet, 1-HyCaRet can be exponentially more succinct than them. Moreover, the complexity of its satisfiability and pushdown model-checking problems are 2Exptime-complete, which is the same complexity as that of two known FO μ -complete extensions of CaRet suitable for compositional and modular reasoning, namely CaRet + ‘within’ and CaRet + ‘forgettable past’. Finally, we show that for each h ≥ 1, satisfiability and pushdown model-checking of the fragment HyCaRet h of HyCaRet consisting of formulas with nesting depth of ∃ at most h is exactly (h+1)-Exptime-complete.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. Logical Methods in Computer Science 4(4) (2008)
Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. 36th STOC, pp. 202–211. ACM, New York (2004)
Alur, R., Madhusudan, P.: Adding nesting structure to words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 1–13. Springer, Heidelberg (2006)
Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model-Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Bozzelli, L., Lanotte, R.: Complexity and succinctness issues for linear-time hybrid logics. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol. 5293, pp. 48–61. Springer, Heidelberg (2008)
Bozzelli, L., Lanotte, R.: Hybrid and first-order complete extensions of CARET. Technical report - (2011), http://dscpi.uninsubria.it/staff/Lanotte
Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 476–491. Springer, Heidelberg (2007)
Bozzelli, L.: Caret with forgettable past. In: Proc. 5th Workshop on Methods for Modalities. ENTCS. Elsevier, Amsterdam (2008)
Franceschet, M., de Rijke, M.: Model checking hybrid logics (with an application to semistructured data). J. Applied Logic 4(3), 279–304 (2006)
Franceschet, M., de Rijke, M., Schlingloff, B.H.: Hybrid logics on linear structures: Expressivity and complexity. In: Proc. 10th TIME, pp. 166–173. IEEE Computer Society, Los Alamitos (2003)
Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proc. 17th LICS, pp. 383–392. IEEE Comp. Soc. Press, Los Alamitos (2002)
Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theoretical Computer Science 148(2), 303–324 (1995)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Schwentick, T., Weber, V.: Bounded-variable fragments of hybrid logics. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 561–572. Springer, Heidelberg (2007)
Wolper, P.: Constructing automata from temporal logic formulas: A tutorial. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 261–277. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bozzelli, L., Lanotte, R. (2011). Hybrid and First-Order Complete Extensions of CaRet . In: Brünnler, K., Metcalfe, G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2011. Lecture Notes in Computer Science(), vol 6793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22119-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-22119-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22118-7
Online ISBN: 978-3-642-22119-4
eBook Packages: Computer ScienceComputer Science (R0)