Space-Efficient Fragments of Higher-Order Fixpoint Logic View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2017-08-25

AUTHORS

Florian Bruse , Martin Lange , Etienne Lozes

ABSTRACT

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed -calculus into the modal -calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most . In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in -EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL. More... »

PAGES

26-41

References to SciGraph publications

  • 1996. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic in CONCUR '96: CONCURRENCY THEORY
  • 2004. A Higher Order Modal Fixed Point Logic in CONCUR 2004 - CONCURRENCY THEORY
  • 2014. Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic in ADVANCED INFORMATION SYSTEMS ENGINEERING
  • 2007. Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic in LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING
  • Book

    TITLE

    Reachability Problems

    ISBN

    978-3-319-67088-1
    978-3-319-67089-8

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3

    DOI

    http://dx.doi.org/10.1007/978-3-319-67089-8_3

    DIMENSIONS

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


    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": "Laboratoire Sp\u00e9cification et V\u00e9rification", 
              "id": "https://www.grid.ac/institutes/grid.464035.0", 
              "name": [
                "University of Kassel, Kassel, Germany", 
                "LSV, ENS Paris-Saclay, CNRS, Cachan, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Bruse", 
            "givenName": "Florian", 
            "id": "sg:person.011477555577.66", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477555577.66"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "University of Kassel", 
              "id": "https://www.grid.ac/institutes/grid.5155.4", 
              "name": [
                "University of Kassel, Kassel, Germany"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Lange", 
            "givenName": "Martin", 
            "id": "sg:person.013644521143.88", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013644521143.88"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Laboratoire Sp\u00e9cification et V\u00e9rification", 
              "id": "https://www.grid.ac/institutes/grid.464035.0", 
              "name": [
                "LSV, ENS Paris-Saclay, CNRS, Cachan, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Lozes", 
            "givenName": "Etienne", 
            "id": "sg:person.014336046241.62", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014336046241.62"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1017/s0956796800003889", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1009194735"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s0956796800003889", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1009194735"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-28644-8_33", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010792135", 
              "https://doi.org/10.1007/978-3-540-28644-8_33"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-28644-8_33", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010792135", 
              "https://doi.org/10.1007/978-3-540-28644-8_33"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-61604-7_60", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1011410166", 
              "https://doi.org/10.1007/3-540-61604-7_60"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/s0022-0000(70)80006-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1017051545"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0190(87)90097-4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1019521827"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0190(87)90097-4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1019521827"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/s0304-3975(98)00314-4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1020192627"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0022-0000(83)90014-4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022042880"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0304-3975(82)90125-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024922185"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.jal.2005.08.002", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1035621913"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.ipl.2006.04.019", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043145663"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1090/s0002-9947-1965-0170805-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1050589417"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-662-44602-7_8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1052220395", 
              "https://doi.org/10.1007/978-3-662-44602-7_8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-75560-9_7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1053125586", 
              "https://doi.org/10.1007/978-3-540-75560-9_7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-75560-9_7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1053125586", 
              "https://doi.org/10.1007/978-3-540-75560-9_7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.2168/lmcs-3(2:7)2007", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1069150905"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/focs.1965.11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1086192375"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2017-08-25", 
        "datePublishedReg": "2017-08-25", 
        "description": "Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed -calculus into the modal -calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most . In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in -EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.", 
        "editor": [
          {
            "familyName": "Hague", 
            "givenName": "Matthew", 
            "type": "Person"
          }, 
          {
            "familyName": "Potapov", 
            "givenName": "Igor", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/978-3-319-67089-8_3", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-319-67088-1", 
            "978-3-319-67089-8"
          ], 
          "name": "Reachability Problems", 
          "type": "Book"
        }, 
        "name": "Space-Efficient Fragments of Higher-Order Fixpoint Logic", 
        "pagination": "26-41", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/978-3-319-67089-8_3"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "533d033a8ac7d8f9d6a1bad34e00449b8cd3c55423d668092a8c3041b682124b"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1091344167"
            ]
          }
        ], 
        "publisher": {
          "location": "Cham", 
          "name": "Springer International Publishing", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/978-3-319-67089-8_3", 
          "https://app.dimensions.ai/details/publication/pub.1091344167"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-16T04:59", 
        "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/0000000325_0000000325/records_100778_00000000.jsonl", 
        "type": "Chapter", 
        "url": "https://link.springer.com/10.1007%2F978-3-319-67089-8_3"
      }
    ]
     

    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/978-3-319-67089-8_3'

    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/978-3-319-67089-8_3'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3'


     

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

    137 TRIPLES      23 PREDICATES      41 URIs      19 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/978-3-319-67089-8_3 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Ncd116007223b49d488c0bffa95e233ed
    4 schema:citation sg:pub.10.1007/3-540-61604-7_60
    5 sg:pub.10.1007/978-3-540-28644-8_33
    6 sg:pub.10.1007/978-3-540-75560-9_7
    7 sg:pub.10.1007/978-3-662-44602-7_8
    8 https://doi.org/10.1016/0020-0190(87)90097-4
    9 https://doi.org/10.1016/0022-0000(83)90014-4
    10 https://doi.org/10.1016/0304-3975(82)90125-6
    11 https://doi.org/10.1016/j.ipl.2006.04.019
    12 https://doi.org/10.1016/j.jal.2005.08.002
    13 https://doi.org/10.1016/s0022-0000(70)80006-x
    14 https://doi.org/10.1016/s0304-3975(98)00314-4
    15 https://doi.org/10.1017/s0956796800003889
    16 https://doi.org/10.1090/s0002-9947-1965-0170805-7
    17 https://doi.org/10.1109/focs.1965.11
    18 https://doi.org/10.2168/lmcs-3(2:7)2007
    19 schema:datePublished 2017-08-25
    20 schema:datePublishedReg 2017-08-25
    21 schema:description Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed -calculus into the modal -calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most . In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in -EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.
    22 schema:editor Nca8121cd776348479827ab222ab1267a
    23 schema:genre chapter
    24 schema:inLanguage en
    25 schema:isAccessibleForFree false
    26 schema:isPartOf N7b16baa3fcc54103b045f0af4cf7436c
    27 schema:name Space-Efficient Fragments of Higher-Order Fixpoint Logic
    28 schema:pagination 26-41
    29 schema:productId N39bc2f0fb7b64c85b88978357b75a114
    30 N655f1e26d5d14eb59749a42d90c63931
    31 N75d316019ae24e5e87f6091dc8f7dc01
    32 schema:publisher Ne114e1d8c8164cebbc87411e23312bcf
    33 schema:sameAs https://app.dimensions.ai/details/publication/pub.1091344167
    34 https://doi.org/10.1007/978-3-319-67089-8_3
    35 schema:sdDatePublished 2019-04-16T04:59
    36 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    37 schema:sdPublisher N186560b9a8674fd4a2ec8de7a4cc8062
    38 schema:url https://link.springer.com/10.1007%2F978-3-319-67089-8_3
    39 sgo:license sg:explorer/license/
    40 sgo:sdDataset chapters
    41 rdf:type schema:Chapter
    42 N063a0284e1eb4d249e90d5faf2d5acdd rdf:first N3d700a4c12b741248fb5d9e140b38a2e
    43 rdf:rest rdf:nil
    44 N186560b9a8674fd4a2ec8de7a4cc8062 schema:name Springer Nature - SN SciGraph project
    45 rdf:type schema:Organization
    46 N2975199cafb04f8398829d88d5874201 rdf:first sg:person.014336046241.62
    47 rdf:rest rdf:nil
    48 N39bc2f0fb7b64c85b88978357b75a114 schema:name dimensions_id
    49 schema:value pub.1091344167
    50 rdf:type schema:PropertyValue
    51 N3ca2244eee8d489f9c1ab9bbe9ef65c0 schema:familyName Hague
    52 schema:givenName Matthew
    53 rdf:type schema:Person
    54 N3d700a4c12b741248fb5d9e140b38a2e schema:familyName Potapov
    55 schema:givenName Igor
    56 rdf:type schema:Person
    57 N655f1e26d5d14eb59749a42d90c63931 schema:name doi
    58 schema:value 10.1007/978-3-319-67089-8_3
    59 rdf:type schema:PropertyValue
    60 N75d316019ae24e5e87f6091dc8f7dc01 schema:name readcube_id
    61 schema:value 533d033a8ac7d8f9d6a1bad34e00449b8cd3c55423d668092a8c3041b682124b
    62 rdf:type schema:PropertyValue
    63 N7b16baa3fcc54103b045f0af4cf7436c schema:isbn 978-3-319-67088-1
    64 978-3-319-67089-8
    65 schema:name Reachability Problems
    66 rdf:type schema:Book
    67 N7fe953c25ff14415865bb3ffb30f0350 rdf:first sg:person.013644521143.88
    68 rdf:rest N2975199cafb04f8398829d88d5874201
    69 Nca8121cd776348479827ab222ab1267a rdf:first N3ca2244eee8d489f9c1ab9bbe9ef65c0
    70 rdf:rest N063a0284e1eb4d249e90d5faf2d5acdd
    71 Ncd116007223b49d488c0bffa95e233ed rdf:first sg:person.011477555577.66
    72 rdf:rest N7fe953c25ff14415865bb3ffb30f0350
    73 Ne114e1d8c8164cebbc87411e23312bcf schema:location Cham
    74 schema:name Springer International Publishing
    75 rdf:type schema:Organisation
    76 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    77 schema:name Information and Computing Sciences
    78 rdf:type schema:DefinedTerm
    79 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    80 schema:name Computation Theory and Mathematics
    81 rdf:type schema:DefinedTerm
    82 sg:person.011477555577.66 schema:affiliation https://www.grid.ac/institutes/grid.464035.0
    83 schema:familyName Bruse
    84 schema:givenName Florian
    85 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477555577.66
    86 rdf:type schema:Person
    87 sg:person.013644521143.88 schema:affiliation https://www.grid.ac/institutes/grid.5155.4
    88 schema:familyName Lange
    89 schema:givenName Martin
    90 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013644521143.88
    91 rdf:type schema:Person
    92 sg:person.014336046241.62 schema:affiliation https://www.grid.ac/institutes/grid.464035.0
    93 schema:familyName Lozes
    94 schema:givenName Etienne
    95 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014336046241.62
    96 rdf:type schema:Person
    97 sg:pub.10.1007/3-540-61604-7_60 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011410166
    98 https://doi.org/10.1007/3-540-61604-7_60
    99 rdf:type schema:CreativeWork
    100 sg:pub.10.1007/978-3-540-28644-8_33 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010792135
    101 https://doi.org/10.1007/978-3-540-28644-8_33
    102 rdf:type schema:CreativeWork
    103 sg:pub.10.1007/978-3-540-75560-9_7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1053125586
    104 https://doi.org/10.1007/978-3-540-75560-9_7
    105 rdf:type schema:CreativeWork
    106 sg:pub.10.1007/978-3-662-44602-7_8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052220395
    107 https://doi.org/10.1007/978-3-662-44602-7_8
    108 rdf:type schema:CreativeWork
    109 https://doi.org/10.1016/0020-0190(87)90097-4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1019521827
    110 rdf:type schema:CreativeWork
    111 https://doi.org/10.1016/0022-0000(83)90014-4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022042880
    112 rdf:type schema:CreativeWork
    113 https://doi.org/10.1016/0304-3975(82)90125-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024922185
    114 rdf:type schema:CreativeWork
    115 https://doi.org/10.1016/j.ipl.2006.04.019 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043145663
    116 rdf:type schema:CreativeWork
    117 https://doi.org/10.1016/j.jal.2005.08.002 schema:sameAs https://app.dimensions.ai/details/publication/pub.1035621913
    118 rdf:type schema:CreativeWork
    119 https://doi.org/10.1016/s0022-0000(70)80006-x schema:sameAs https://app.dimensions.ai/details/publication/pub.1017051545
    120 rdf:type schema:CreativeWork
    121 https://doi.org/10.1016/s0304-3975(98)00314-4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020192627
    122 rdf:type schema:CreativeWork
    123 https://doi.org/10.1017/s0956796800003889 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009194735
    124 rdf:type schema:CreativeWork
    125 https://doi.org/10.1090/s0002-9947-1965-0170805-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1050589417
    126 rdf:type schema:CreativeWork
    127 https://doi.org/10.1109/focs.1965.11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1086192375
    128 rdf:type schema:CreativeWork
    129 https://doi.org/10.2168/lmcs-3(2:7)2007 schema:sameAs https://app.dimensions.ai/details/publication/pub.1069150905
    130 rdf:type schema:CreativeWork
    131 https://www.grid.ac/institutes/grid.464035.0 schema:alternateName Laboratoire Spécification et Vérification
    132 schema:name LSV, ENS Paris-Saclay, CNRS, Cachan, France
    133 University of Kassel, Kassel, Germany
    134 rdf:type schema:Organization
    135 https://www.grid.ac/institutes/grid.5155.4 schema:alternateName University of Kassel
    136 schema:name University of Kassel, Kassel, Germany
    137 rdf:type schema:Organization
     




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


    ...