A game-based abstraction-refinement framework for Markov decision processes View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2010-08-03

AUTHORS

Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, David Parker

ABSTRACT

In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for an abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies. More... »

PAGES

246-280

References to SciGraph publications

  • 2007. Magnifying-Lens Abstraction for Markov Decision Processes in COMPUTER AIDED VERIFICATION
  • 2004. Analysing Randomized Distributed Algorithms in VALIDATION OF STOCHASTIC SYSTEMS
  • 2006. Model-Checking Markov Chains in the Presence of Uncertainties in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2004. An Abstraction Framework for Mixed Non-deterministic and Probabilistic Systems in VALIDATION OF STOCHASTIC SYSTEMS
  • 1976. Denumerable Markov Chains, with a chapter of Markov Random Fields by David Griffeath in NONE
  • 2008-01-01. Probabilistic CEGAR in COMPUTER AIDED VERIFICATION
  • 1999-04-30. Root Contention in IEEE 1394 in FORMAL METHODS FOR REAL-TIME AND PROBABILISTIC SYSTEMS
  • 2006. PRISM: A Tool for Automatic Verification of Probabilistic Systems in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 1998-08. Model checking for a probabilistic branching time logic with fairness in DISTRIBUTED COMPUTING
  • 1999. Computing Minimum and Maximum Reachability Times in Probabilistic Systems in CONCUR’99 CONCURRENCY THEORY
  • 2006. Don’t Know in Probabilistic Systems in MODEL CHECKING SOFTWARE
  • 2006-06-07. Performance analysis of probabilistic timed automata using digital clocks in FORMAL METHODS IN SYSTEM DESIGN
  • 2010. Best Probabilistic Transformers in VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION
  • 1997. Construction of abstract state graphs with PVS in COMPUTER AIDED VERIFICATION
  • 2001-08-30. Reachability Analysis of Probabilistic Systems by Successive Refinements in PROCESS ALGEBRA AND PROBABILISTIC METHODS. PERFORMANCE MODELLING AND VERIFICATION
  • 2000. Counterexample-Guided Abstraction Refinement in COMPUTER AIDED VERIFICATION
  • 2009. Stochastic Games for Verification of Probabilistic Timed Automata in FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS
  • 2007. Abstract Interpretation for Worst and Average Case Analysis in PROGRAM ANALYSIS AND COMPILATION, THEORY AND PRACTICE
  • 2008. Abstraction Refinement for Probabilistic Software in VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s10703-010-0097-6

    DOI

    http://dx.doi.org/10.1007/s10703-010-0097-6

    DIMENSIONS

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


    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/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
              "id": "http://www.grid.ac/institutes/grid.4991.5", 
              "name": [
                "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Kattenbelt", 
            "givenName": "Mark", 
            "id": "sg:person.010521117025.43", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010521117025.43"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
              "id": "http://www.grid.ac/institutes/grid.4991.5", 
              "name": [
                "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Kwiatkowska", 
            "givenName": "Marta", 
            "id": "sg:person.011375012273.39", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Department of Computing Science, University of Glasgow, 18 Lilybank Gardens, Glasgow, G12 8RZ, Scotland", 
              "id": "http://www.grid.ac/institutes/grid.8756.c", 
              "name": [
                "Department of Computing Science, University of Glasgow, 18 Lilybank Gardens, Glasgow, G12 8RZ, Scotland"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Norman", 
            "givenName": "Gethin", 
            "id": "sg:person.016323171577.36", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK", 
              "id": "http://www.grid.ac/institutes/grid.4991.5", 
              "name": [
                "Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Parker", 
            "givenName": "David", 
            "id": "sg:person.014007552600.37", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/11691372_29", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1017058917", 
              "https://doi.org/10.1007/11691372_29"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-71322-7_8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1035328259", 
              "https://doi.org/10.1007/978-3-540-71322-7_8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-1-4684-9455-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1003855982", 
              "https://doi.org/10.1007/978-1-4684-9455-6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-24611-4_12", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038265187", 
              "https://doi.org/10.1007/978-3-540-24611-4_12"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-44804-7_3", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1029771156", 
              "https://doi.org/10.1007/3-540-44804-7_3"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-04368-0_17", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027948650", 
              "https://doi.org/10.1007/978-3-642-04368-0_17"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s004460050046", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022009982", 
              "https://doi.org/10.1007/s004460050046"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11691372_26", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1040209951", 
              "https://doi.org/10.1007/11691372_26"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-24611-4_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1031779578", 
              "https://doi.org/10.1007/978-3-540-24611-4_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/10722167_15", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1021635428", 
              "https://doi.org/10.1007/10722167_15"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-93900-9_17", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041083442", 
              "https://doi.org/10.1007/978-3-540-93900-9_17"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11691617_5", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1050242585", 
              "https://doi.org/10.1007/11691617_5"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-48320-9_7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030350626", 
              "https://doi.org/10.1007/3-540-48320-9_7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-73368-3_38", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034509510", 
              "https://doi.org/10.1007/978-3-540-73368-3_38"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-48778-6_4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049686904", 
              "https://doi.org/10.1007/3-540-48778-6_4"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-006-0005-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002395349", 
              "https://doi.org/10.1007/s10703-006-0005-2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-70545-1_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044553785", 
              "https://doi.org/10.1007/978-3-540-70545-1_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-11319-2_26", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1001722883", 
              "https://doi.org/10.1007/978-3-642-11319-2_26"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-63166-6_10", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008574754", 
              "https://doi.org/10.1007/3-540-63166-6_10"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2010-08-03", 
        "datePublishedReg": "2010-08-03", 
        "description": "In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for an abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s10703-010-0097-6", 
        "inLanguage": "en", 
        "isAccessibleForFree": true, 
        "isFundedItemOf": [
          {
            "id": "sg:grant.2772676", 
            "type": "MonetaryGrant"
          }, 
          {
            "id": "sg:grant.2767392", 
            "type": "MonetaryGrant"
          }, 
          {
            "id": "sg:grant.2777727", 
            "type": "MonetaryGrant"
          }, 
          {
            "id": "sg:grant.2756180", 
            "type": "MonetaryGrant"
          }
        ], 
        "isPartOf": [
          {
            "id": "sg:journal.1052628", 
            "issn": [
              "0925-9856", 
              "1572-8102"
            ], 
            "name": "Formal Methods in System Design", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "3", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "36"
          }
        ], 
        "keywords": [
          "Markov decision process", 
          "abstraction-refinement framework", 
          "abstraction approach", 
          "state space explosion problem", 
          "real-world case study", 
          "abstraction refinement loop", 
          "decision process", 
          "original Markov decision process", 
          "prototype implementation", 
          "automatic generation", 
          "model checking", 
          "probabilistic verification", 
          "little practical progress", 
          "nondeterministic behavior", 
          "abstraction refinement", 
          "two-player game", 
          "explosion problem", 
          "efficient algorithm", 
          "reachability properties", 
          "key idea", 
          "refinement method", 
          "successful methodology", 
          "present experimental results", 
          "abstraction process", 
          "different players", 
          "experimental results", 
          "nondeterminism", 
          "abstraction", 
          "framework", 
          "game", 
          "large selection", 
          "upper bounds", 
          "checking", 
          "practical progress", 
          "case study", 
          "algorithm", 
          "verification", 
          "implementation", 
          "quantitative measures", 
          "method", 
          "methodology", 
          "process", 
          "system", 
          "bounds", 
          "idea", 
          "modelling", 
          "players", 
          "selection", 
          "quality", 
          "refinement", 
          "generation", 
          "field", 
          "results", 
          "progress", 
          "setting", 
          "loop", 
          "basis", 
          "measures", 
          "types", 
          "behavior", 
          "values", 
          "properties", 
          "study", 
          "separation", 
          "problem", 
          "approach", 
          "paper"
        ], 
        "name": "A game-based abstraction-refinement framework for Markov decision processes", 
        "pagination": "246-280", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1013198998"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s10703-010-0097-6"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s10703-010-0097-6", 
          "https://app.dimensions.ai/details/publication/pub.1013198998"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-05-20T07:26", 
        "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/article/article_520.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s10703-010-0097-6"
      }
    ]
     

    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/s10703-010-0097-6'

    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/s10703-010-0097-6'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10703-010-0097-6'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10703-010-0097-6'


     

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

    233 TRIPLES      22 PREDICATES      111 URIs      84 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s10703-010-0097-6 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author N77bb12354651416db368bf25fa4fe599
    4 schema:citation sg:pub.10.1007/10722167_15
    5 sg:pub.10.1007/11691372_26
    6 sg:pub.10.1007/11691372_29
    7 sg:pub.10.1007/11691617_5
    8 sg:pub.10.1007/3-540-44804-7_3
    9 sg:pub.10.1007/3-540-48320-9_7
    10 sg:pub.10.1007/3-540-48778-6_4
    11 sg:pub.10.1007/3-540-63166-6_10
    12 sg:pub.10.1007/978-1-4684-9455-6
    13 sg:pub.10.1007/978-3-540-24611-4_11
    14 sg:pub.10.1007/978-3-540-24611-4_12
    15 sg:pub.10.1007/978-3-540-70545-1_16
    16 sg:pub.10.1007/978-3-540-71322-7_8
    17 sg:pub.10.1007/978-3-540-73368-3_38
    18 sg:pub.10.1007/978-3-540-93900-9_17
    19 sg:pub.10.1007/978-3-642-04368-0_17
    20 sg:pub.10.1007/978-3-642-11319-2_26
    21 sg:pub.10.1007/s004460050046
    22 sg:pub.10.1007/s10703-006-0005-2
    23 schema:datePublished 2010-08-03
    24 schema:datePublishedReg 2010-08-03
    25 schema:description In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for an abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies.
    26 schema:genre article
    27 schema:inLanguage en
    28 schema:isAccessibleForFree true
    29 schema:isPartOf N27bb9ff8aca14335bd5d75dbad4c8058
    30 N288385e226d7455a956cdc8dfb8db9a1
    31 sg:journal.1052628
    32 schema:keywords Markov decision process
    33 abstraction
    34 abstraction approach
    35 abstraction process
    36 abstraction refinement
    37 abstraction refinement loop
    38 abstraction-refinement framework
    39 algorithm
    40 approach
    41 automatic generation
    42 basis
    43 behavior
    44 bounds
    45 case study
    46 checking
    47 decision process
    48 different players
    49 efficient algorithm
    50 experimental results
    51 explosion problem
    52 field
    53 framework
    54 game
    55 generation
    56 idea
    57 implementation
    58 key idea
    59 large selection
    60 little practical progress
    61 loop
    62 measures
    63 method
    64 methodology
    65 model checking
    66 modelling
    67 nondeterminism
    68 nondeterministic behavior
    69 original Markov decision process
    70 paper
    71 players
    72 practical progress
    73 present experimental results
    74 probabilistic verification
    75 problem
    76 process
    77 progress
    78 properties
    79 prototype implementation
    80 quality
    81 quantitative measures
    82 reachability properties
    83 real-world case study
    84 refinement
    85 refinement method
    86 results
    87 selection
    88 separation
    89 setting
    90 state space explosion problem
    91 study
    92 successful methodology
    93 system
    94 two-player game
    95 types
    96 upper bounds
    97 values
    98 verification
    99 schema:name A game-based abstraction-refinement framework for Markov decision processes
    100 schema:pagination 246-280
    101 schema:productId N86225340ab67446a86b2d1062788aca7
    102 Ne0a698ffcf2e45a886a9fa1764b98e25
    103 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013198998
    104 https://doi.org/10.1007/s10703-010-0097-6
    105 schema:sdDatePublished 2022-05-20T07:26
    106 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    107 schema:sdPublisher N8da76cf56a5547b399037aee828479df
    108 schema:url https://doi.org/10.1007/s10703-010-0097-6
    109 sgo:license sg:explorer/license/
    110 sgo:sdDataset articles
    111 rdf:type schema:ScholarlyArticle
    112 N27bb9ff8aca14335bd5d75dbad4c8058 schema:issueNumber 3
    113 rdf:type schema:PublicationIssue
    114 N288385e226d7455a956cdc8dfb8db9a1 schema:volumeNumber 36
    115 rdf:type schema:PublicationVolume
    116 N4d7b661c129245e090d151c813a73ca5 rdf:first sg:person.011375012273.39
    117 rdf:rest N959b35d7b84f4b93905ed33012bc9634
    118 N534a7681579d4969a011e069acfae814 rdf:first sg:person.014007552600.37
    119 rdf:rest rdf:nil
    120 N77bb12354651416db368bf25fa4fe599 rdf:first sg:person.010521117025.43
    121 rdf:rest N4d7b661c129245e090d151c813a73ca5
    122 N86225340ab67446a86b2d1062788aca7 schema:name doi
    123 schema:value 10.1007/s10703-010-0097-6
    124 rdf:type schema:PropertyValue
    125 N8da76cf56a5547b399037aee828479df schema:name Springer Nature - SN SciGraph project
    126 rdf:type schema:Organization
    127 N959b35d7b84f4b93905ed33012bc9634 rdf:first sg:person.016323171577.36
    128 rdf:rest N534a7681579d4969a011e069acfae814
    129 Ne0a698ffcf2e45a886a9fa1764b98e25 schema:name dimensions_id
    130 schema:value pub.1013198998
    131 rdf:type schema:PropertyValue
    132 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    133 schema:name Information and Computing Sciences
    134 rdf:type schema:DefinedTerm
    135 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    136 schema:name Computation Theory and Mathematics
    137 rdf:type schema:DefinedTerm
    138 sg:grant.2756180 http://pending.schema.org/fundedItem sg:pub.10.1007/s10703-010-0097-6
    139 rdf:type schema:MonetaryGrant
    140 sg:grant.2767392 http://pending.schema.org/fundedItem sg:pub.10.1007/s10703-010-0097-6
    141 rdf:type schema:MonetaryGrant
    142 sg:grant.2772676 http://pending.schema.org/fundedItem sg:pub.10.1007/s10703-010-0097-6
    143 rdf:type schema:MonetaryGrant
    144 sg:grant.2777727 http://pending.schema.org/fundedItem sg:pub.10.1007/s10703-010-0097-6
    145 rdf:type schema:MonetaryGrant
    146 sg:journal.1052628 schema:issn 0925-9856
    147 1572-8102
    148 schema:name Formal Methods in System Design
    149 schema:publisher Springer Nature
    150 rdf:type schema:Periodical
    151 sg:person.010521117025.43 schema:affiliation grid-institutes:grid.4991.5
    152 schema:familyName Kattenbelt
    153 schema:givenName Mark
    154 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010521117025.43
    155 rdf:type schema:Person
    156 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
    157 schema:familyName Kwiatkowska
    158 schema:givenName Marta
    159 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
    160 rdf:type schema:Person
    161 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.4991.5
    162 schema:familyName Parker
    163 schema:givenName David
    164 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
    165 rdf:type schema:Person
    166 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
    167 schema:familyName Norman
    168 schema:givenName Gethin
    169 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
    170 rdf:type schema:Person
    171 sg:pub.10.1007/10722167_15 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021635428
    172 https://doi.org/10.1007/10722167_15
    173 rdf:type schema:CreativeWork
    174 sg:pub.10.1007/11691372_26 schema:sameAs https://app.dimensions.ai/details/publication/pub.1040209951
    175 https://doi.org/10.1007/11691372_26
    176 rdf:type schema:CreativeWork
    177 sg:pub.10.1007/11691372_29 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017058917
    178 https://doi.org/10.1007/11691372_29
    179 rdf:type schema:CreativeWork
    180 sg:pub.10.1007/11691617_5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1050242585
    181 https://doi.org/10.1007/11691617_5
    182 rdf:type schema:CreativeWork
    183 sg:pub.10.1007/3-540-44804-7_3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1029771156
    184 https://doi.org/10.1007/3-540-44804-7_3
    185 rdf:type schema:CreativeWork
    186 sg:pub.10.1007/3-540-48320-9_7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030350626
    187 https://doi.org/10.1007/3-540-48320-9_7
    188 rdf:type schema:CreativeWork
    189 sg:pub.10.1007/3-540-48778-6_4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049686904
    190 https://doi.org/10.1007/3-540-48778-6_4
    191 rdf:type schema:CreativeWork
    192 sg:pub.10.1007/3-540-63166-6_10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008574754
    193 https://doi.org/10.1007/3-540-63166-6_10
    194 rdf:type schema:CreativeWork
    195 sg:pub.10.1007/978-1-4684-9455-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003855982
    196 https://doi.org/10.1007/978-1-4684-9455-6
    197 rdf:type schema:CreativeWork
    198 sg:pub.10.1007/978-3-540-24611-4_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031779578
    199 https://doi.org/10.1007/978-3-540-24611-4_11
    200 rdf:type schema:CreativeWork
    201 sg:pub.10.1007/978-3-540-24611-4_12 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038265187
    202 https://doi.org/10.1007/978-3-540-24611-4_12
    203 rdf:type schema:CreativeWork
    204 sg:pub.10.1007/978-3-540-70545-1_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044553785
    205 https://doi.org/10.1007/978-3-540-70545-1_16
    206 rdf:type schema:CreativeWork
    207 sg:pub.10.1007/978-3-540-71322-7_8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1035328259
    208 https://doi.org/10.1007/978-3-540-71322-7_8
    209 rdf:type schema:CreativeWork
    210 sg:pub.10.1007/978-3-540-73368-3_38 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034509510
    211 https://doi.org/10.1007/978-3-540-73368-3_38
    212 rdf:type schema:CreativeWork
    213 sg:pub.10.1007/978-3-540-93900-9_17 schema:sameAs https://app.dimensions.ai/details/publication/pub.1041083442
    214 https://doi.org/10.1007/978-3-540-93900-9_17
    215 rdf:type schema:CreativeWork
    216 sg:pub.10.1007/978-3-642-04368-0_17 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027948650
    217 https://doi.org/10.1007/978-3-642-04368-0_17
    218 rdf:type schema:CreativeWork
    219 sg:pub.10.1007/978-3-642-11319-2_26 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001722883
    220 https://doi.org/10.1007/978-3-642-11319-2_26
    221 rdf:type schema:CreativeWork
    222 sg:pub.10.1007/s004460050046 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022009982
    223 https://doi.org/10.1007/s004460050046
    224 rdf:type schema:CreativeWork
    225 sg:pub.10.1007/s10703-006-0005-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002395349
    226 https://doi.org/10.1007/s10703-006-0005-2
    227 rdf:type schema:CreativeWork
    228 grid-institutes:grid.4991.5 schema:alternateName Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK
    229 schema:name Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK
    230 rdf:type schema:Organization
    231 grid-institutes:grid.8756.c schema:alternateName Department of Computing Science, University of Glasgow, 18 Lilybank Gardens, Glasgow, G12 8RZ, Scotland
    232 schema:name Department of Computing Science, University of Glasgow, 18 Lilybank Gardens, Glasgow, G12 8RZ, Scotland
    233 rdf:type schema:Organization
     




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


    ...