Model checking dynamic pushdown networks View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2015-03

AUTHORS

Fu Song, Tayssir Touili

ABSTRACT

A dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread creation. Thus, it is important to have model checking algorithms for DPNs. We consider in this work model checking DPNs against single-indexed LTL and CTL properties of the form ⋀fi such that fi is a LTL/CTL formula over the PDS i. We consider the model checking problems w.r.t. simple valuations (i.e., whether a configuration satisfies an atomic proposition depends only on its control location) and w.r.t. regular valuations (i.e., the set of the configurations satisfying an atomic proposition is a regular set of configurations). We show that these model checking problems are decidable. We propose automata-based approaches for computing the set of configurations of a DPN that satisfy the corresponding single-indexed LTL/CTL formula. More... »

PAGES

397-421

References to SciGraph publications

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/s00165-014-0330-y

DOI

http://dx.doi.org/10.1007/s00165-014-0330-y

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1006100551


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "East China Normal University", 
          "id": "https://www.grid.ac/institutes/grid.22069.3f", 
          "name": [
            "Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, No. 3663 Zhongshan Road(N), Shanghai, People\u2019s Republic of China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Song", 
        "givenName": "Fu", 
        "id": "sg:person.011106004607.30", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011106004607.30"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Laboratoire d'Informatique Algorithmique: Fondements et Applications", 
          "id": "https://www.grid.ac/institutes/grid.462842.e", 
          "name": [
            "Liafa, CNRS and Universit\u00e9 Paris Diderot, Paris, France"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Touili", 
        "givenName": "Tayssir", 
        "id": "sg:person.013251045351.38", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013251045351.38"
        ], 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "sg:pub.10.1007/s00236-008-0082-3", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1010200828", 
          "https://doi.org/10.1007/s00236-008-0082-3"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/s00236-008-0082-3", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1010200828", 
          "https://doi.org/10.1007/s00236-008-0082-3"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0022-0000(86)90026-7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1011826113"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1006/inco.1999.2826", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1036308864"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/j.tcs.2010.05.028", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1040567871"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/s0890-5401(03)00139-1", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1043908684"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/s0890-5401(03)00139-1", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1043908684"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1142/s0129054111008453", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062897127"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "2015-03", 
    "datePublishedReg": "2015-03-01", 
    "description": "A dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread creation. Thus, it is important to have model checking algorithms for DPNs. We consider in this work model checking DPNs against single-indexed LTL and CTL properties of the form \u22c0fi such that fi is a LTL/CTL formula over the PDS i. We consider the model checking problems w.r.t. simple valuations (i.e., whether a configuration satisfies an atomic proposition depends only on its control location) and w.r.t. regular valuations (i.e., the set of the configurations satisfying an atomic proposition is a regular set of configurations). We show that these model checking problems are decidable. We propose automata-based approaches for computing the set of configurations of a DPN that satisfy the corresponding single-indexed LTL/CTL formula.", 
    "genre": "research_article", 
    "id": "sg:pub.10.1007/s00165-014-0330-y", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": false, 
    "isPartOf": [
      {
        "id": "sg:journal.1136737", 
        "issn": [
          "0934-5043", 
          "1433-299X"
        ], 
        "name": "Formal Aspects of Computing", 
        "type": "Periodical"
      }, 
      {
        "issueNumber": "2", 
        "type": "PublicationIssue"
      }, 
      {
        "type": "PublicationVolume", 
        "volumeNumber": "27"
      }
    ], 
    "name": "Model checking dynamic pushdown networks", 
    "pagination": "397-421", 
    "productId": [
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "1d0fa4c0cdd0211c646df4780bfa5b3256443e40396d230b16f26c4c126ac992"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/s00165-014-0330-y"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1006100551"
        ]
      }
    ], 
    "sameAs": [
      "https://doi.org/10.1007/s00165-014-0330-y", 
      "https://app.dimensions.ai/details/publication/pub.1006100551"
    ], 
    "sdDataset": "articles", 
    "sdDatePublished": "2019-04-10T13:04", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000001_0000000264/records_8659_00000480.jsonl", 
    "type": "ScholarlyArticle", 
    "url": "http://link.springer.com/10.1007/s00165-014-0330-y"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/s00165-014-0330-y'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/s00165-014-0330-y'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s00165-014-0330-y'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s00165-014-0330-y'


 

This table displays all metadata directly associated to this object as RDF triples.

90 TRIPLES      21 PREDICATES      33 URIs      19 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/s00165-014-0330-y schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Nbeca10ea38eb44f19bc291b0f5498bef
4 schema:citation sg:pub.10.1007/s00236-008-0082-3
5 https://doi.org/10.1006/inco.1999.2826
6 https://doi.org/10.1016/0022-0000(86)90026-7
7 https://doi.org/10.1016/j.tcs.2010.05.028
8 https://doi.org/10.1016/s0890-5401(03)00139-1
9 https://doi.org/10.1142/s0129054111008453
10 schema:datePublished 2015-03
11 schema:datePublishedReg 2015-03-01
12 schema:description A dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread creation. Thus, it is important to have model checking algorithms for DPNs. We consider in this work model checking DPNs against single-indexed LTL and CTL properties of the form ⋀fi such that fi is a LTL/CTL formula over the PDS i. We consider the model checking problems w.r.t. simple valuations (i.e., whether a configuration satisfies an atomic proposition depends only on its control location) and w.r.t. regular valuations (i.e., the set of the configurations satisfying an atomic proposition is a regular set of configurations). We show that these model checking problems are decidable. We propose automata-based approaches for computing the set of configurations of a DPN that satisfy the corresponding single-indexed LTL/CTL formula.
13 schema:genre research_article
14 schema:inLanguage en
15 schema:isAccessibleForFree false
16 schema:isPartOf N192a6d712d524802b5018ef73ede220b
17 N238ab557024e4a4f8cc7b8e88e32828c
18 sg:journal.1136737
19 schema:name Model checking dynamic pushdown networks
20 schema:pagination 397-421
21 schema:productId N4c3addfa6ed147ac803cf71ed4001c42
22 Nbb05c70f01014155a88af0350a502a4d
23 Nbdbb7cd3e70e48b8823827d31343fc65
24 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006100551
25 https://doi.org/10.1007/s00165-014-0330-y
26 schema:sdDatePublished 2019-04-10T13:04
27 schema:sdLicense https://scigraph.springernature.com/explorer/license/
28 schema:sdPublisher N3cae9f8515344d86bb81e5cb6a74902d
29 schema:url http://link.springer.com/10.1007/s00165-014-0330-y
30 sgo:license sg:explorer/license/
31 sgo:sdDataset articles
32 rdf:type schema:ScholarlyArticle
33 N192a6d712d524802b5018ef73ede220b schema:issueNumber 2
34 rdf:type schema:PublicationIssue
35 N22c872236d56468180cbbdbe234bedc1 rdf:first sg:person.013251045351.38
36 rdf:rest rdf:nil
37 N238ab557024e4a4f8cc7b8e88e32828c schema:volumeNumber 27
38 rdf:type schema:PublicationVolume
39 N3cae9f8515344d86bb81e5cb6a74902d schema:name Springer Nature - SN SciGraph project
40 rdf:type schema:Organization
41 N4c3addfa6ed147ac803cf71ed4001c42 schema:name readcube_id
42 schema:value 1d0fa4c0cdd0211c646df4780bfa5b3256443e40396d230b16f26c4c126ac992
43 rdf:type schema:PropertyValue
44 Nbb05c70f01014155a88af0350a502a4d schema:name dimensions_id
45 schema:value pub.1006100551
46 rdf:type schema:PropertyValue
47 Nbdbb7cd3e70e48b8823827d31343fc65 schema:name doi
48 schema:value 10.1007/s00165-014-0330-y
49 rdf:type schema:PropertyValue
50 Nbeca10ea38eb44f19bc291b0f5498bef rdf:first sg:person.011106004607.30
51 rdf:rest N22c872236d56468180cbbdbe234bedc1
52 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
53 schema:name Information and Computing Sciences
54 rdf:type schema:DefinedTerm
55 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
56 schema:name Computation Theory and Mathematics
57 rdf:type schema:DefinedTerm
58 sg:journal.1136737 schema:issn 0934-5043
59 1433-299X
60 schema:name Formal Aspects of Computing
61 rdf:type schema:Periodical
62 sg:person.011106004607.30 schema:affiliation https://www.grid.ac/institutes/grid.22069.3f
63 schema:familyName Song
64 schema:givenName Fu
65 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011106004607.30
66 rdf:type schema:Person
67 sg:person.013251045351.38 schema:affiliation https://www.grid.ac/institutes/grid.462842.e
68 schema:familyName Touili
69 schema:givenName Tayssir
70 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013251045351.38
71 rdf:type schema:Person
72 sg:pub.10.1007/s00236-008-0082-3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010200828
73 https://doi.org/10.1007/s00236-008-0082-3
74 rdf:type schema:CreativeWork
75 https://doi.org/10.1006/inco.1999.2826 schema:sameAs https://app.dimensions.ai/details/publication/pub.1036308864
76 rdf:type schema:CreativeWork
77 https://doi.org/10.1016/0022-0000(86)90026-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011826113
78 rdf:type schema:CreativeWork
79 https://doi.org/10.1016/j.tcs.2010.05.028 schema:sameAs https://app.dimensions.ai/details/publication/pub.1040567871
80 rdf:type schema:CreativeWork
81 https://doi.org/10.1016/s0890-5401(03)00139-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043908684
82 rdf:type schema:CreativeWork
83 https://doi.org/10.1142/s0129054111008453 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062897127
84 rdf:type schema:CreativeWork
85 https://www.grid.ac/institutes/grid.22069.3f schema:alternateName East China Normal University
86 schema:name Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, No. 3663 Zhongshan Road(N), Shanghai, People’s Republic of China
87 rdf:type schema:Organization
88 https://www.grid.ac/institutes/grid.462842.e schema:alternateName Laboratoire d'Informatique Algorithmique: Fondements et Applications
89 schema:name Liafa, CNRS and Université Paris Diderot, Paris, France
90 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...