Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds* View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2002-03-15

AUTHORS

Petr Jančar , Antonín Kučera , Faron Moller , Zdeněk Sawa

ABSTRACT

We present a general method for proving DP-hardness of equivalencechecking problems on one-counter automata. For this we show a reduction of the Sat-Unsat problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains only special formulas with one free variable, and is particularly apt for transforming to simulation-like equivalences on onecounter automata. In this way we show that the membership problem for any relation subsuming bisimilarity and subsumed by simulation preorder is DP-hard (even) for one-counter nets (where the counter cannot be tested for zero).We also show DP-hardness for deciding simulation between one-counter automata and finite-state systems (in both directions). More... »

PAGES

172-186

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/3-540-45931-6_13

DOI

http://dx.doi.org/10.1007/3-540-45931-6_13

DIMENSIONS

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


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/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Dept. of Computer Science, FEI, Technical University of Ostrava, 17. listopadu 15, CZ-708 33, Ostrava, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.440850.d", 
          "name": [
            "Dept. of Computer Science, FEI, Technical University of Ostrava, 17. listopadu 15, CZ-708 33, Ostrava, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Jan\u010dar", 
        "givenName": "Petr", 
        "id": "sg:person.07724710171.43", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07724710171.43"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, CZ-602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, CZ-602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ku\u010dera", 
        "givenName": "Anton\u00edn", 
        "id": "sg:person.012453075541.89", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012453075541.89"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Dept. of Computer Science, University of Wales Swansea, Singleton Park, SA2 8PP, Swansea, Wales", 
          "id": "http://www.grid.ac/institutes/grid.4827.9", 
          "name": [
            "Dept. of Computer Science, University of Wales Swansea, Singleton Park, SA2 8PP, Swansea, Wales"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Moller", 
        "givenName": "Faron", 
        "id": "sg:person.010425236217.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Dept. of Computer Science, FEI, Technical University of Ostrava, 17. listopadu 15, CZ-708 33, Ostrava, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.440850.d", 
          "name": [
            "Dept. of Computer Science, FEI, Technical University of Ostrava, 17. listopadu 15, CZ-708 33, Ostrava, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Sawa", 
        "givenName": "Zden\u011bk", 
        "id": "sg:person.016412231345.81", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016412231345.81"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2002-03-15", 
    "datePublishedReg": "2002-03-15", 
    "description": "We present a general method for proving DP-hardness of equivalencechecking problems on one-counter automata. For this we show a reduction of the Sat-Unsat problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains only special formulas with one free variable, and is particularly apt for transforming to simulation-like equivalences on onecounter automata. In this way we show that the membership problem for any relation subsuming bisimilarity and subsumed by simulation preorder is DP-hard (even) for one-counter nets (where the counter cannot be tested for zero).We also show DP-hardness for deciding simulation between one-counter automata and finite-state systems (in both directions).", 
    "editor": [
      {
        "familyName": "Nielsen", 
        "givenName": "Mogens", 
        "type": "Person"
      }, 
      {
        "familyName": "Engberg", 
        "givenName": "Uffe", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/3-540-45931-6_13", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-43366-8", 
        "978-3-540-45931-6"
      ], 
      "name": "Foundations of Software Science and Computation Structures", 
      "type": "Book"
    }, 
    "keywords": [
      "finite-state systems", 
      "one-counter automata", 
      "simulation preorder", 
      "one-counter nets", 
      "generic method", 
      "automata", 
      "truth problem", 
      "membership problem", 
      "free variables", 
      "Lower Bound", 
      "nets", 
      "general method", 
      "bisimilarity", 
      "method", 
      "preorder", 
      "system", 
      "bounds", 
      "simulations", 
      "way", 
      "equivalence", 
      "special formula", 
      "variables", 
      "formula", 
      "relation", 
      "reduction", 
      "DP", 
      "fragments", 
      "problem"
    ], 
    "name": "Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds*", 
    "pagination": "172-186", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1007133095"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/3-540-45931-6_13"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/3-540-45931-6_13", 
      "https://app.dimensions.ai/details/publication/pub.1007133095"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:49", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/chapter/chapter_82.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/3-540-45931-6_13"
  }
]
 

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/3-540-45931-6_13'

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/3-540-45931-6_13'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-45931-6_13'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/3-540-45931-6_13'


 

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

120 TRIPLES      23 PREDICATES      53 URIs      46 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/3-540-45931-6_13 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 schema:author N3a96a2bd75f74bf8af18b3e1e22571a1
4 schema:datePublished 2002-03-15
5 schema:datePublishedReg 2002-03-15
6 schema:description We present a general method for proving DP-hardness of equivalencechecking problems on one-counter automata. For this we show a reduction of the Sat-Unsat problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains only special formulas with one free variable, and is particularly apt for transforming to simulation-like equivalences on onecounter automata. In this way we show that the membership problem for any relation subsuming bisimilarity and subsumed by simulation preorder is DP-hard (even) for one-counter nets (where the counter cannot be tested for zero).We also show DP-hardness for deciding simulation between one-counter automata and finite-state systems (in both directions).
7 schema:editor Nb36aa52498324de9b9fc0173c530c83e
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N810239301d634c119e653ea68e37e3ee
12 schema:keywords DP
13 Lower Bound
14 automata
15 bisimilarity
16 bounds
17 equivalence
18 finite-state systems
19 formula
20 fragments
21 free variables
22 general method
23 generic method
24 membership problem
25 method
26 nets
27 one-counter automata
28 one-counter nets
29 preorder
30 problem
31 reduction
32 relation
33 simulation preorder
34 simulations
35 special formula
36 system
37 truth problem
38 variables
39 way
40 schema:name Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds*
41 schema:pagination 172-186
42 schema:productId N7be24c7607e940188a414e30695c52e7
43 N831abd3589954cd6aa6d06036ab024f5
44 schema:publisher N402fabd972db476d89d33d855bc22156
45 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007133095
46 https://doi.org/10.1007/3-540-45931-6_13
47 schema:sdDatePublished 2022-05-20T07:49
48 schema:sdLicense https://scigraph.springernature.com/explorer/license/
49 schema:sdPublisher Nf0d8c51eef9e4284a0fd19da5650886f
50 schema:url https://doi.org/10.1007/3-540-45931-6_13
51 sgo:license sg:explorer/license/
52 sgo:sdDataset chapters
53 rdf:type schema:Chapter
54 N06403768bc6d494ab00018c47b373da6 schema:familyName Nielsen
55 schema:givenName Mogens
56 rdf:type schema:Person
57 N3a96a2bd75f74bf8af18b3e1e22571a1 rdf:first sg:person.07724710171.43
58 rdf:rest Nf0e43bd9d2a74ebc8c643228ce8773de
59 N402fabd972db476d89d33d855bc22156 schema:name Springer Nature
60 rdf:type schema:Organisation
61 N6162133430c04557984fbefbbd44ce87 rdf:first N925d26f1df154e9c999206ba5c873ab8
62 rdf:rest rdf:nil
63 N7be24c7607e940188a414e30695c52e7 schema:name dimensions_id
64 schema:value pub.1007133095
65 rdf:type schema:PropertyValue
66 N7e116a77cd554484b28e3833d7bc1890 rdf:first sg:person.010425236217.29
67 rdf:rest N98ca515e8da54ab99d084e26d773df73
68 N810239301d634c119e653ea68e37e3ee schema:isbn 978-3-540-43366-8
69 978-3-540-45931-6
70 schema:name Foundations of Software Science and Computation Structures
71 rdf:type schema:Book
72 N831abd3589954cd6aa6d06036ab024f5 schema:name doi
73 schema:value 10.1007/3-540-45931-6_13
74 rdf:type schema:PropertyValue
75 N925d26f1df154e9c999206ba5c873ab8 schema:familyName Engberg
76 schema:givenName Uffe
77 rdf:type schema:Person
78 N98ca515e8da54ab99d084e26d773df73 rdf:first sg:person.016412231345.81
79 rdf:rest rdf:nil
80 Nb36aa52498324de9b9fc0173c530c83e rdf:first N06403768bc6d494ab00018c47b373da6
81 rdf:rest N6162133430c04557984fbefbbd44ce87
82 Nf0d8c51eef9e4284a0fd19da5650886f schema:name Springer Nature - SN SciGraph project
83 rdf:type schema:Organization
84 Nf0e43bd9d2a74ebc8c643228ce8773de rdf:first sg:person.012453075541.89
85 rdf:rest N7e116a77cd554484b28e3833d7bc1890
86 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
87 schema:name Information and Computing Sciences
88 rdf:type schema:DefinedTerm
89 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
90 schema:name Artificial Intelligence and Image Processing
91 rdf:type schema:DefinedTerm
92 sg:person.010425236217.29 schema:affiliation grid-institutes:grid.4827.9
93 schema:familyName Moller
94 schema:givenName Faron
95 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010425236217.29
96 rdf:type schema:Person
97 sg:person.012453075541.89 schema:affiliation grid-institutes:grid.10267.32
98 schema:familyName Kučera
99 schema:givenName Antonín
100 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012453075541.89
101 rdf:type schema:Person
102 sg:person.016412231345.81 schema:affiliation grid-institutes:grid.440850.d
103 schema:familyName Sawa
104 schema:givenName Zdeněk
105 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016412231345.81
106 rdf:type schema:Person
107 sg:person.07724710171.43 schema:affiliation grid-institutes:grid.440850.d
108 schema:familyName Jančar
109 schema:givenName Petr
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07724710171.43
111 rdf:type schema:Person
112 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Botanická 68a, CZ-602 00, Brno, Czech Republic
113 schema:name Faculty of Informatics, Masaryk University, Botanická 68a, CZ-602 00, Brno, Czech Republic
114 rdf:type schema:Organization
115 grid-institutes:grid.440850.d schema:alternateName Dept. of Computer Science, FEI, Technical University of Ostrava, 17. listopadu 15, CZ-708 33, Ostrava, Czech Republic
116 schema:name Dept. of Computer Science, FEI, Technical University of Ostrava, 17. listopadu 15, CZ-708 33, Ostrava, Czech Republic
117 rdf:type schema:Organization
118 grid-institutes:grid.4827.9 schema:alternateName Dept. of Computer Science, University of Wales Swansea, Singleton Park, SA2 8PP, Swansea, Wales
119 schema:name Dept. of Computer Science, University of Wales Swansea, Singleton Park, SA2 8PP, Swansea, Wales
120 rdf:type schema:Organization
 




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


...