Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twenty-First Annual IEEE Symposium on

Logic in Computer Science (LICS 2006)

Paper: Monadic chain logic over iterations and applications to pushdown systems (at LICS 2006)

Authors: Dietrich Kuske Markus Lohrey

Abstract

Logical properties of iterations of relational structures are studied and these decidability results are applied to the model checking of a powerful extension of pushdown systems. It is shown that the monadic chain theory of the iteration of a structure A (in the sense of Shelah and Stupp) is decidable in case the first-order theory of the structure A is decidable. This result fails if Muchnik’s clone-predicate is added. A model of pushdown automata, where the stack alphabet is given by an arbitrary (possibly infinite) relational structure, is introduced. If the stack structure has a decidable first-order theory with regular reachability predicates, then the same holds for the configuration graph of this pushdown automaton. This result follows from our decidability result for the monadic chain theory of the iteration.

BibTeX

  @InProceedings{KuskeLohrey-Monadicchainlogicov,
    author = 	 {Dietrich Kuske and Markus Lohrey},
    title = 	 {Monadic chain logic over iterations and applications to pushdown systems},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {91--100},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski