Model-Checking by Infinite Fly-Automata

作者: Bruno Courcelle , Irène Durand

DOI: 10.1007/978-3-642-40663-8_20

关键词:

摘要: We present logic based methods for constructing XP and FPT graph algorithms, parameterized by tree-width or clique-width. will use fly-automata introduced in a previous article. They make it possible to check properties that are not monadic second-order expressible because their states may include counters, so set of be infinite. equip these automata with output functions, they can compute values associated terms graphs. tools easily algorithms combining predefined basic functions properties.

参考文章(16)
Bruno Courcelle, Irène Durand, Computations by fly-automata beyond monadic second-order logic Theoretical Computer Science. ,vol. 619, pp. 32- 67 ,(2016) , 10.1016/J.TCS.2015.12.026
Margus Veanes, Nikolaj Bjørner, Symbolic automata: the toolkit tools and algorithms for construction and analysis of systems. pp. 472- 477 ,(2012) , 10.1007/978-3-642-28756-5_33
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Klaus Reinhardt, The complexity of translating logic to finite automata Lecture Notes in Computer Science. pp. 231- 238 ,(2002) , 10.1007/3-540-36387-4_13
Michael R. Fellows, Fedor V. Fomin, Daniel Lokshtanov, Frances Rosamond, Saket Saurabh, Stefan Szeider, Carsten Thomassen, On the complexity of some colorful problems parameterized by treewidth Information & Computation. ,vol. 209, pp. 143- 153 ,(2011) , 10.1016/J.IC.2010.11.026
Michaël Rao, MSOL partitioning problems on graphs of bounded treewidth and clique-width Theoretical Computer Science. ,vol. 377, pp. 260- 267 ,(2007) , 10.1016/J.TCS.2007.03.043
B. Courcelle, M. Mosbah, Monadic second-order evaluations on tree-decomposable graphs Theoretical Computer Science. ,vol. 109, pp. 49- 82 ,(1993) , 10.1016/0304-3975(93)90064-Z
Bruno Courcelle, Irène Durand, Automata for the verification of monadic second-order graph properties Journal of Applied Logic. ,vol. 10, pp. 368- 409 ,(2012) , 10.1016/J.JAL.2011.07.001
B. Courcelle, J. A. Makowsky, U. Rotics, Linear Time Solvable Optimization Problems on Graphs of Bounded Clique-Width Theory of Computing Systems \/ Mathematical Systems Theory. ,vol. 33, pp. 125- 150 ,(2000) , 10.1007/S002249910009