Model Checking Languages of Data Words

Benedikt Bollig; Aiswarya Cyriac; Paul Gastin; K. Narayan Kumar

hal-00658333, version 1

Model Checking Languages of Data Words

Benedikt Bollig (, ) ^1, 2, Aiswarya Cyriac () ^1, 2, Paul Gastin () ^1, 2, K. Narayan Kumar () ³

FoSSaCS 2012 (2012) to appear

Abstract: We consider the model-checking problem for data multi-pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic.

1: Laboratoire Spécification et Vérification [Cachan] (LSV)
CNRS : UMR8643 – INRIA – École normale supérieure de Cachan - ENS Cachan
2: MEXICO (INRIA Saclay - Ile de France)
INRIA – École normale supérieure de Cachan - ENS Cachan – CNRS : UMR8643
3: Chennai Mathematical Institute [Inde]
Chennai Mathematical Institute

hal-00658333, version 1
http://hal.archives-ouvertes.fr/hal-00658333
oai:hal.archives-ouvertes.fr:hal-00658333
From: Benedikt Bollig <>
Submitted on: Tuesday, 10 January 2012 13:06:42
Updated on: Wednesday, 16 January 2013 11:01:39

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00658333"><analytic>
<author><persName><forename>Benedikt</forename><surname>Bollig</surname></persName>
<affiliation>
<orgName type="laboratory">LSV</orgName>
<orgName type="team">Laboratoire Spécification et Vérification [Cachan]</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR8643</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">MEXICO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
<orgName type="institution">CNRS : UMR8643</orgName>
</affiliation>
</author>
<author><persName><forename>Aiswarya</forename><surname>Cyriac</surname></persName>
<affiliation>
<orgName type="laboratory">LSV</orgName>
<orgName type="team">Laboratoire Spécification et Vérification [Cachan]</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR8643</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">MEXICO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
<orgName type="institution">CNRS : UMR8643</orgName>
</affiliation>
</author>
<author><persName><forename>Paul</forename><surname>Gastin</surname></persName>
<affiliation>
<orgName type="laboratory">LSV</orgName>
<orgName type="team">Laboratoire Spécification et Vérification [Cachan]</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR8643</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Saclay - Ile de France</orgName>
<orgName type="team">MEXICO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">École normale supérieure de Cachan - ENS Cachan</orgName>
<orgName type="institution">CNRS : UMR8643</orgName>
</affiliation>
</author>
<author><persName><forename>K.</forename><surname>Narayan Kumar</surname></persName>
<affiliation>
<orgName type="team">Chennai Mathematical Institute [Inde]</orgName>
<country>IN</country>
<orgName type="institution">Chennai Mathematical Institute</orgName>
</affiliation>
</author>
<title type="main" level="a">Model Checking Languages of Data Words</title></analytic><monogr><title level="m" type="main">FoSSaCS 2012</title><meeting>FoSSaCS 2012</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Tallinn</settlement><country>Estonia</country></pubPlace><biblScope type="publicationDate">2012-03-00</biblScope><biblScope type="pp">to appear</biblScope></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00658333</idno><idno type="HALFile">http://hal.archives-ouvertes.fr/hal-00658333/PDF/modelchecking.pdf</idno></biblStruct>
</listBibl>
</listBibl>