A Weighted MSO Logic with Storage Behaviour and Its Büchi-Elgot-Trakhtenbrot Theorem

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

A Weighted MSO Logic with Storage Behaviour and Its Büchi-Elgot-Trakhtenbrot Theorem

Heiko VoglerHeiko Vogler,  Manfred DrosteManfred Droste,  Luisa HerrmannLuisa Herrmann
Heiko Vogler, Manfred Droste, Luisa Herrmann
A Weighted MSO Logic with Storage Behaviour and Its Büchi-Elgot-Trakhtenbrot Theorem
In Adrian-Horia DediuJan Janoušek, Carlos Martín-Vide, Bianca Truthe, eds., Language and Automata Theory and Applications, volume 9618 of Lecture Notes in Computer Science, 127-139, 2016. Springer
  • KurzfassungAbstract
    We introduce a weighted MSO-logic in which one outermost existential quantification over behaviours of a storage type is allowed. As weight structures we take unital valuation monoids which include all semirings, bounded lattices, and computations of average or discounted costs. Each formula is interpreted over finite words yielding elements in the weight structure. We prove that this logic is expressively equivalent to weighted automata with storage. In particular, this implies a Büchi-Elgot-Trakhtenbrot Theorem for weighted iterated pushdown languages. For this choice of storage type, the satisfiability problem of the logic is decidable for each bounded lattice provided that its infimum is computable.
  • Projekt:Project: QuantLA
  • Forschungsgruppe:Research Group: Computational LogicComputational Logic
The final publication is available at Springer via http://dx.doi.org/https://doi.org/10.1007/978-3-319-30000-9_10.
@inproceedings{VDH2016,
  author    = {Heiko Vogler and Manfred Droste and Luisa Herrmann},
  title     = {A Weighted {MSO} Logic with Storage Behaviour and Its
               B{\"{u}}chi-Elgot-Trakhtenbrot Theorem},
  editor    = {Adrian-Horia {DediuJan} Janou{\v{s}}ek and Carlos
               Mart{\'{\i}}n-Vide and Bianca Truthe},
  booktitle = {Language and Automata Theory and Applications},
  series    = {Lecture Notes in Computer Science},
  volume    = {9618},
  publisher = {Springer},
  year      = {2016},
  pages     = {127-139},
  doi       = {https://doi.org/10.1007/978-3-319-30000-9_10}
}