Abstract
We define an action-based extension of the branching-time temporal logic CTL which allows path quantifiers to be restricted by formal languages. The main purpose of this logic is its use in abstract interpretation. A reduction from a concrete system to an abstract one may contain spurious traces which can render the verification of the abstract system useless with respect to the concrete one. We pick up the suggestion to verify a modified property on the abstract system instead of the one that the concrete system is supposed to have. The logic introduced here enables a systematic modification of such properties. We present some ways of such a modification which aim at implicitly excluding spurious traces in the verification of abstracted systems.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. 36th Ann. ACM Symp. on Theory of Computing, STOC 2004, pp. 202–211 (2004)
Bosnacki, D., Ioustinova, N., Sidorova, N.: Using fairness to make abstractions work. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 198–215. Springer, Heidelberg (2004)
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)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Congress on Logic, Method, and Philosophy of Science, pp. 1–12. Stanford University Press, Stanford (1962)
Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50(5), 752–794 (2003)
Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30, 1–24 (1985)
Emerson, E.A., Halpern, J.Y.: “sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)
Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. In: Annual IEEE Symposium on Foundations of Computer Science, pp. 328–337 (1988)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)
Löding, C., Lutz, C., Serre, O.: Propositional dynamic logic with recursive programs. J. Log. Algebr. Program. 73(1-2), 51–69 (2007)
Löding, C., Serre, O.: Propositional dynamic logic with recursive programs. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 292–306. Springer, Heidelberg (2006)
De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th Symp. on Foundations of Computer Science, FOCS 1977, Providence, RI, USA, pp. 46–57. IEEE, Los Alamitos (1977)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the Association for Computing Machinery 32(3), 733–749 (1985)
Staiger, L.: Handbook of formal languages. In: ω-languages. Beyond words, vol. 3, pp. 339–387. Springer, Heidelberg (1997)
Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control 54(1/2), 121–141 (1982)
Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 183–221 (1986)
Walukiewicz, I.: Pushdown processes: Games and model-checking. Information and Computation 164(2), 234–263 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lange, M., Latte, M. (2010). A CTL-Based Logic for Program Abstractions. In: Dawar, A., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2010. Lecture Notes in Computer Science(), vol 6188. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13824-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-13824-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13823-2
Online ISBN: 978-3-642-13824-9
eBook Packages: Computer ScienceComputer Science (R0)