Model checking for probabilistic timed automata View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2012-10-12

AUTHORS

Gethin Norman, David Parker, Jeremy Sproston

ABSTRACT

Probabilistic timed automata (PTAs) are a formalism for modelling systems whose behaviour incorporates both probabilistic and real-time characteristics. Applications include wireless communication protocols, automotive network protocols and randomised security protocols. This paper gives an introduction to PTAs and describes techniques for analysing a wide range of quantitative properties, such as “the maximum probability of the airbag failing to deploy within 0.02 seconds”, “the maximum expected time for the protocol to terminate” or “the minimum expected energy consumption required to complete all tasks”. We present a temporal logic for specifying such properties and then give a survey of available model-checking techniques for formulae specified in this logic. We then describe two case studies in which PTAs are used for modelling and analysis: a probabilistic non-repudiation protocol and a task-graph scheduling problem. More... »

PAGES

164-190

References to SciGraph publications

  • 1995. Model checking of probabilistic and nondeterministic systems in FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE
  • 2011. Automated Verification Techniques for Probabilistic Systems in FORMAL METHODS FOR ETERNAL NETWORKED SOFTWARE SYSTEMS
  • 2009. Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata in THEORY AND APPLICATIONS OF MODELS OF COMPUTATION
  • 1998-08. Model checking for a probabilistic branching time logic with fairness in DISTRIBUTED COMPUTING
  • 1994. Probabilistic simulations for probabilistic processes in CONCUR '94: CONCURRENCY THEORY
  • 2006-06-07. Performance analysis of probabilistic timed automata using digital clocks in FORMAL METHODS IN SYSTEM DESIGN
  • 2002-09-05. Interactive Markov Chains, And the Quest for Quantified Quality in NONE
  • 1994-09. A logic for reasoning about time and reliability in FORMAL ASPECTS OF COMPUTING
  • 1992. Minimization of timed transition systems in CONCUR '92
  • 2009. Concavely-Priced Probabilistic Timed Automata in CONCUR 2009 - CONCURRENCY THEORY
  • 2009. Strict Divergence for Probabilistic Timed Automata in CONCUR 2009 - CONCURRENCY THEORY
  • 2008-01-01. Modeling and Validation of Aviation Security in INTELLIGENCE AND SECURITY INFORMATICS
  • 2007-12-05. Optimal infinite scheduling for multi-priced timed automata in FORMAL METHODS IN SYSTEM DESIGN
  • 1999-04-30. Verifying Progress in Timed Systems in FORMAL METHODS FOR REAL-TIME AND PROBABILISTIC SYSTEMS
  • 2001-03-16. Improvements in BDD-Based Reachability Analysis of Timed Automata in FME 2001: FORMAL METHODS FOR INCREASING SOFTWARE PRODUCTIVITY
  • 1992. What good are digital clocks? in AUTOMATA, LANGUAGES AND PROGRAMMING
  • 2003-04. Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol in FORMAL ASPECTS OF COMPUTING
  • 2012-08-03. An extension of the inverse method to probabilistic timed automata in FORMAL METHODS IN SYSTEM DESIGN
  • 2009. Stochastic Games for Verification of Probabilistic Timed Automata in FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS
  • 2003-02-17. Untameable Timed Automata! in STACS 2003
  • 2000-12-21. Verifying Quantitative Properties of Continuous Probabilistic Timed Automata in CONCUR 2000 — CONCURRENCY THEORY
  • 1982. Design and synthesis of synchronization skeletons using branching time temporal logic in LOGICS OF PROGRAMS
  • 2001-03-21. Minimum-Cost Reachability for Priced Time Automata in HYBRID SYSTEMS: COMPUTATION AND CONTROL
  • 1991. Model-checking for probabilistic real-time systems in AUTOMATA, LANGUAGES AND PROGRAMMING
  • 2007. UPPAAL-Tiga: Time for Playing Games! in COMPUTER AIDED VERIFICATION
  • 2005-05. Checking Timed Büchi Automata Emptiness Efficiently in FORMAL METHODS IN SYSTEM DESIGN
  • 2010-08-03. A game-based abstraction-refinement framework for Markov decision processes in FORMAL METHODS IN SYSTEM DESIGN
  • 1976. Denumerable Markov Chains, with a chapter of Markov Random Fields by David Griffeath in NONE
  • 1998. On discretization of delays in timed automata and digital circuits in CONCUR'98 CONCURRENCY THEORY
  • 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems in COMPUTER AIDED VERIFICATION
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s10703-012-0177-x

    DOI

    http://dx.doi.org/10.1007/s10703-012-0177-x

    DIMENSIONS

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


    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": "School of Computing Science, University of Glasgow, 18 Lilybank Gardens, G12 8RZ, Glasgow, Scotland, UK", 
              "id": "http://www.grid.ac/institutes/grid.8756.c", 
              "name": [
                "School of Computing Science, University of Glasgow, 18 Lilybank Gardens, G12 8RZ, Glasgow, Scotland, UK"
              ], 
              "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": "School of Computer Science, University of Birmingham, Edgbaston, B15 2TT, Birmingham, UK", 
              "id": "http://www.grid.ac/institutes/grid.6572.6", 
              "name": [
                "School of Computer Science, University of Birmingham, Edgbaston, B15 2TT, Birmingham, 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"
          }, 
          {
            "affiliation": {
              "alternateName": "Dipartimento di Informatica, Universit\u00e0 degli Studi di Torino, Corso Svizzera 185, 10149, Torino, Italy", 
              "id": "http://www.grid.ac/institutes/grid.7605.4", 
              "name": [
                "Dipartimento di Informatica, Universit\u00e0 degli Studi di Torino, Corso Svizzera 185, 10149, Torino, Italy"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Sproston", 
            "givenName": "Jeremy", 
            "id": "sg:person.014412237577.02", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014412237577.02"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/bfb0084802", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1000746222", 
              "https://doi.org/10.1007/bfb0084802"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-005-1632-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1017423314", 
              "https://doi.org/10.1007/s10703-005-1632-8"
            ], 
            "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/3-540-45351-2_15", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002788038", 
              "https://doi.org/10.1007/3-540-45351-2_15"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-60692-0_70", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022695129", 
              "https://doi.org/10.1007/3-540-60692-0_70"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-010-0097-6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1013198998", 
              "https://doi.org/10.1007/s10703-010-0097-6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-36494-3_54", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027122372", 
              "https://doi.org/10.1007/3-540-36494-3_54"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s001650300007", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1036098084", 
              "https://doi.org/10.1007/s001650300007"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-22110-1_47", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027900693", 
              "https://doi.org/10.1007/978-3-642-22110-1_47"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-73368-3_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004409162", 
              "https://doi.org/10.1007/978-3-540-73368-3_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0025774", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1037700041", 
              "https://doi.org/10.1007/bfb0025774"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-007-0043-4", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018321911", 
              "https://doi.org/10.1007/s10703-007-0043-4"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0015027", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1023196586", 
              "https://doi.org/10.1007/bfb0015027"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01211866", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1052049375", 
              "https://doi.org/10.1007/bf01211866"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-21455-4_3", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1043781609", 
              "https://doi.org/10.1007/978-3-642-21455-4_3"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-48778-6_18", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1026111332", 
              "https://doi.org/10.1007/3-540-48778-6_18"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-54233-7_128", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012557000", 
              "https://doi.org/10.1007/3-540-54233-7_128"
            ], 
            "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/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-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/3-540-45804-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1015609309", 
              "https://doi.org/10.1007/3-540-45804-2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-55719-9_103", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1006689972", 
              "https://doi.org/10.1007/3-540-55719-9_103"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10703-012-0169-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1025479965", 
              "https://doi.org/10.1007/s10703-012-0169-x"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-04081-8_41", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1009347576", 
              "https://doi.org/10.1007/978-3-642-04081-8_41"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-45251-6_18", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1049472072", 
              "https://doi.org/10.1007/3-540-45251-6_18"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-44618-4_11", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044044194", 
              "https://doi.org/10.1007/3-540-44618-4_11"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-04081-8_28", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004314002", 
              "https://doi.org/10.1007/978-3-642-04081-8_28"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-02017-9_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1052923504", 
              "https://doi.org/10.1007/978-3-642-02017-9_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-69209-6_18", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008954548", 
              "https://doi.org/10.1007/978-3-540-69209-6_18"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0055642", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1052557339", 
              "https://doi.org/10.1007/bfb0055642"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2012-10-12", 
        "datePublishedReg": "2012-10-12", 
        "description": "Probabilistic timed automata (PTAs) are a formalism for modelling systems whose behaviour incorporates both probabilistic and real-time characteristics. Applications include wireless communication protocols, automotive network protocols and randomised security protocols. This paper gives an introduction to PTAs and describes techniques for analysing a wide range of quantitative properties, such as \u201cthe maximum probability of the airbag failing to deploy within 0.02 seconds\u201d, \u201cthe maximum expected time for the protocol to terminate\u201d or \u201cthe minimum expected energy consumption required to complete all tasks\u201d. We present a temporal logic for specifying such properties and then give a survey of available model-checking techniques for formulae specified in this logic. We then describe two case studies in which PTAs are used for modelling and analysis: a probabilistic non-repudiation protocol and a task-graph scheduling problem.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s10703-012-0177-x", 
        "inLanguage": "en", 
        "isAccessibleForFree": true, 
        "isPartOf": [
          {
            "id": "sg:journal.1052628", 
            "issn": [
              "0925-9856", 
              "1572-8102"
            ], 
            "name": "Formal Methods in System Design", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "43"
          }
        ], 
        "keywords": [
          "model-checking techniques", 
          "wireless communication protocols", 
          "real-time characteristics", 
          "task graph scheduling problems", 
          "security protocols", 
          "probabilistic non-repudiation protocol", 
          "network protocols", 
          "non-repudiation protocol", 
          "communication protocols", 
          "temporal logic", 
          "scheduling problem", 
          "energy consumption", 
          "automata", 
          "logic", 
          "quantitative properties", 
          "protocol", 
          "maximum probability", 
          "case study", 
          "task", 
          "technique", 
          "such properties", 
          "applications", 
          "wide range", 
          "system", 
          "modelling", 
          "formalism", 
          "seconds", 
          "model", 
          "consumption", 
          "probability", 
          "airbag", 
          "time", 
          "introduction", 
          "behavior", 
          "characteristics", 
          "analysis", 
          "minimum", 
          "PTA", 
          "survey", 
          "formula", 
          "properties", 
          "range", 
          "study", 
          "problem", 
          "paper"
        ], 
        "name": "Model checking for probabilistic timed automata", 
        "pagination": "164-190", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1047241468"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s10703-012-0177-x"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s10703-012-0177-x", 
          "https://app.dimensions.ai/details/publication/pub.1047241468"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-05-10T10:05", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/article/article_557.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s10703-012-0177-x"
      }
    ]
     

    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-012-0177-x'

    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-012-0177-x'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10703-012-0177-x'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10703-012-0177-x'


     

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

    243 TRIPLES      22 PREDICATES      100 URIs      62 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s10703-012-0177-x schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author N5f527125c712444eb0d47c44d229cb82
    4 schema:citation sg:pub.10.1007/3-540-36494-3_54
    5 sg:pub.10.1007/3-540-44618-4_11
    6 sg:pub.10.1007/3-540-45251-6_18
    7 sg:pub.10.1007/3-540-45351-2_15
    8 sg:pub.10.1007/3-540-45804-2
    9 sg:pub.10.1007/3-540-48778-6_18
    10 sg:pub.10.1007/3-540-54233-7_128
    11 sg:pub.10.1007/3-540-55719-9_103
    12 sg:pub.10.1007/3-540-60692-0_70
    13 sg:pub.10.1007/978-1-4684-9455-6
    14 sg:pub.10.1007/978-3-540-69209-6_18
    15 sg:pub.10.1007/978-3-540-73368-3_14
    16 sg:pub.10.1007/978-3-642-02017-9_16
    17 sg:pub.10.1007/978-3-642-04081-8_28
    18 sg:pub.10.1007/978-3-642-04081-8_41
    19 sg:pub.10.1007/978-3-642-04368-0_17
    20 sg:pub.10.1007/978-3-642-21455-4_3
    21 sg:pub.10.1007/978-3-642-22110-1_47
    22 sg:pub.10.1007/bf01211866
    23 sg:pub.10.1007/bfb0015027
    24 sg:pub.10.1007/bfb0025774
    25 sg:pub.10.1007/bfb0055642
    26 sg:pub.10.1007/bfb0084802
    27 sg:pub.10.1007/s001650300007
    28 sg:pub.10.1007/s004460050046
    29 sg:pub.10.1007/s10703-005-1632-8
    30 sg:pub.10.1007/s10703-006-0005-2
    31 sg:pub.10.1007/s10703-007-0043-4
    32 sg:pub.10.1007/s10703-010-0097-6
    33 sg:pub.10.1007/s10703-012-0169-x
    34 schema:datePublished 2012-10-12
    35 schema:datePublishedReg 2012-10-12
    36 schema:description Probabilistic timed automata (PTAs) are a formalism for modelling systems whose behaviour incorporates both probabilistic and real-time characteristics. Applications include wireless communication protocols, automotive network protocols and randomised security protocols. This paper gives an introduction to PTAs and describes techniques for analysing a wide range of quantitative properties, such as “the maximum probability of the airbag failing to deploy within 0.02 seconds”, “the maximum expected time for the protocol to terminate” or “the minimum expected energy consumption required to complete all tasks”. We present a temporal logic for specifying such properties and then give a survey of available model-checking techniques for formulae specified in this logic. We then describe two case studies in which PTAs are used for modelling and analysis: a probabilistic non-repudiation protocol and a task-graph scheduling problem.
    37 schema:genre article
    38 schema:inLanguage en
    39 schema:isAccessibleForFree true
    40 schema:isPartOf N4cc40cd122a3421a99a01256730940d3
    41 N618c93cd24fd44f590cc47e675b07309
    42 sg:journal.1052628
    43 schema:keywords PTA
    44 airbag
    45 analysis
    46 applications
    47 automata
    48 behavior
    49 case study
    50 characteristics
    51 communication protocols
    52 consumption
    53 energy consumption
    54 formalism
    55 formula
    56 introduction
    57 logic
    58 maximum probability
    59 minimum
    60 model
    61 model-checking techniques
    62 modelling
    63 network protocols
    64 non-repudiation protocol
    65 paper
    66 probabilistic non-repudiation protocol
    67 probability
    68 problem
    69 properties
    70 protocol
    71 quantitative properties
    72 range
    73 real-time characteristics
    74 scheduling problem
    75 seconds
    76 security protocols
    77 study
    78 such properties
    79 survey
    80 system
    81 task
    82 task graph scheduling problems
    83 technique
    84 temporal logic
    85 time
    86 wide range
    87 wireless communication protocols
    88 schema:name Model checking for probabilistic timed automata
    89 schema:pagination 164-190
    90 schema:productId N8058cfa32dc94547a14ac58ecce90861
    91 Nbf987ba97a524bc18557611d9814dd83
    92 schema:sameAs https://app.dimensions.ai/details/publication/pub.1047241468
    93 https://doi.org/10.1007/s10703-012-0177-x
    94 schema:sdDatePublished 2022-05-10T10:05
    95 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    96 schema:sdPublisher Ne5d55460770f4bde81593c472e3c1912
    97 schema:url https://doi.org/10.1007/s10703-012-0177-x
    98 sgo:license sg:explorer/license/
    99 sgo:sdDataset articles
    100 rdf:type schema:ScholarlyArticle
    101 N0fbde7bcc2d74e77b20ff7d8ecb12089 rdf:first sg:person.014007552600.37
    102 rdf:rest N743fce02c16d48069aaa28b16772aa32
    103 N4cc40cd122a3421a99a01256730940d3 schema:volumeNumber 43
    104 rdf:type schema:PublicationVolume
    105 N5f527125c712444eb0d47c44d229cb82 rdf:first sg:person.016323171577.36
    106 rdf:rest N0fbde7bcc2d74e77b20ff7d8ecb12089
    107 N618c93cd24fd44f590cc47e675b07309 schema:issueNumber 2
    108 rdf:type schema:PublicationIssue
    109 N743fce02c16d48069aaa28b16772aa32 rdf:first sg:person.014412237577.02
    110 rdf:rest rdf:nil
    111 N8058cfa32dc94547a14ac58ecce90861 schema:name dimensions_id
    112 schema:value pub.1047241468
    113 rdf:type schema:PropertyValue
    114 Nbf987ba97a524bc18557611d9814dd83 schema:name doi
    115 schema:value 10.1007/s10703-012-0177-x
    116 rdf:type schema:PropertyValue
    117 Ne5d55460770f4bde81593c472e3c1912 schema:name Springer Nature - SN SciGraph project
    118 rdf:type schema:Organization
    119 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    120 schema:name Information and Computing Sciences
    121 rdf:type schema:DefinedTerm
    122 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    123 schema:name Computation Theory and Mathematics
    124 rdf:type schema:DefinedTerm
    125 sg:journal.1052628 schema:issn 0925-9856
    126 1572-8102
    127 schema:name Formal Methods in System Design
    128 schema:publisher Springer Nature
    129 rdf:type schema:Periodical
    130 sg:person.014007552600.37 schema:affiliation grid-institutes:grid.6572.6
    131 schema:familyName Parker
    132 schema:givenName David
    133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014007552600.37
    134 rdf:type schema:Person
    135 sg:person.014412237577.02 schema:affiliation grid-institutes:grid.7605.4
    136 schema:familyName Sproston
    137 schema:givenName Jeremy
    138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014412237577.02
    139 rdf:type schema:Person
    140 sg:person.016323171577.36 schema:affiliation grid-institutes:grid.8756.c
    141 schema:familyName Norman
    142 schema:givenName Gethin
    143 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016323171577.36
    144 rdf:type schema:Person
    145 sg:pub.10.1007/3-540-36494-3_54 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027122372
    146 https://doi.org/10.1007/3-540-36494-3_54
    147 rdf:type schema:CreativeWork
    148 sg:pub.10.1007/3-540-44618-4_11 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044044194
    149 https://doi.org/10.1007/3-540-44618-4_11
    150 rdf:type schema:CreativeWork
    151 sg:pub.10.1007/3-540-45251-6_18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049472072
    152 https://doi.org/10.1007/3-540-45251-6_18
    153 rdf:type schema:CreativeWork
    154 sg:pub.10.1007/3-540-45351-2_15 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002788038
    155 https://doi.org/10.1007/3-540-45351-2_15
    156 rdf:type schema:CreativeWork
    157 sg:pub.10.1007/3-540-45804-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1015609309
    158 https://doi.org/10.1007/3-540-45804-2
    159 rdf:type schema:CreativeWork
    160 sg:pub.10.1007/3-540-48778-6_18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1026111332
    161 https://doi.org/10.1007/3-540-48778-6_18
    162 rdf:type schema:CreativeWork
    163 sg:pub.10.1007/3-540-54233-7_128 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012557000
    164 https://doi.org/10.1007/3-540-54233-7_128
    165 rdf:type schema:CreativeWork
    166 sg:pub.10.1007/3-540-55719-9_103 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006689972
    167 https://doi.org/10.1007/3-540-55719-9_103
    168 rdf:type schema:CreativeWork
    169 sg:pub.10.1007/3-540-60692-0_70 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022695129
    170 https://doi.org/10.1007/3-540-60692-0_70
    171 rdf:type schema:CreativeWork
    172 sg:pub.10.1007/978-1-4684-9455-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003855982
    173 https://doi.org/10.1007/978-1-4684-9455-6
    174 rdf:type schema:CreativeWork
    175 sg:pub.10.1007/978-3-540-69209-6_18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008954548
    176 https://doi.org/10.1007/978-3-540-69209-6_18
    177 rdf:type schema:CreativeWork
    178 sg:pub.10.1007/978-3-540-73368-3_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004409162
    179 https://doi.org/10.1007/978-3-540-73368-3_14
    180 rdf:type schema:CreativeWork
    181 sg:pub.10.1007/978-3-642-02017-9_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052923504
    182 https://doi.org/10.1007/978-3-642-02017-9_16
    183 rdf:type schema:CreativeWork
    184 sg:pub.10.1007/978-3-642-04081-8_28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004314002
    185 https://doi.org/10.1007/978-3-642-04081-8_28
    186 rdf:type schema:CreativeWork
    187 sg:pub.10.1007/978-3-642-04081-8_41 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009347576
    188 https://doi.org/10.1007/978-3-642-04081-8_41
    189 rdf:type schema:CreativeWork
    190 sg:pub.10.1007/978-3-642-04368-0_17 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027948650
    191 https://doi.org/10.1007/978-3-642-04368-0_17
    192 rdf:type schema:CreativeWork
    193 sg:pub.10.1007/978-3-642-21455-4_3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043781609
    194 https://doi.org/10.1007/978-3-642-21455-4_3
    195 rdf:type schema:CreativeWork
    196 sg:pub.10.1007/978-3-642-22110-1_47 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027900693
    197 https://doi.org/10.1007/978-3-642-22110-1_47
    198 rdf:type schema:CreativeWork
    199 sg:pub.10.1007/bf01211866 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052049375
    200 https://doi.org/10.1007/bf01211866
    201 rdf:type schema:CreativeWork
    202 sg:pub.10.1007/bfb0015027 schema:sameAs https://app.dimensions.ai/details/publication/pub.1023196586
    203 https://doi.org/10.1007/bfb0015027
    204 rdf:type schema:CreativeWork
    205 sg:pub.10.1007/bfb0025774 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037700041
    206 https://doi.org/10.1007/bfb0025774
    207 rdf:type schema:CreativeWork
    208 sg:pub.10.1007/bfb0055642 schema:sameAs https://app.dimensions.ai/details/publication/pub.1052557339
    209 https://doi.org/10.1007/bfb0055642
    210 rdf:type schema:CreativeWork
    211 sg:pub.10.1007/bfb0084802 schema:sameAs https://app.dimensions.ai/details/publication/pub.1000746222
    212 https://doi.org/10.1007/bfb0084802
    213 rdf:type schema:CreativeWork
    214 sg:pub.10.1007/s001650300007 schema:sameAs https://app.dimensions.ai/details/publication/pub.1036098084
    215 https://doi.org/10.1007/s001650300007
    216 rdf:type schema:CreativeWork
    217 sg:pub.10.1007/s004460050046 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022009982
    218 https://doi.org/10.1007/s004460050046
    219 rdf:type schema:CreativeWork
    220 sg:pub.10.1007/s10703-005-1632-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017423314
    221 https://doi.org/10.1007/s10703-005-1632-8
    222 rdf:type schema:CreativeWork
    223 sg:pub.10.1007/s10703-006-0005-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002395349
    224 https://doi.org/10.1007/s10703-006-0005-2
    225 rdf:type schema:CreativeWork
    226 sg:pub.10.1007/s10703-007-0043-4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018321911
    227 https://doi.org/10.1007/s10703-007-0043-4
    228 rdf:type schema:CreativeWork
    229 sg:pub.10.1007/s10703-010-0097-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013198998
    230 https://doi.org/10.1007/s10703-010-0097-6
    231 rdf:type schema:CreativeWork
    232 sg:pub.10.1007/s10703-012-0169-x schema:sameAs https://app.dimensions.ai/details/publication/pub.1025479965
    233 https://doi.org/10.1007/s10703-012-0169-x
    234 rdf:type schema:CreativeWork
    235 grid-institutes:grid.6572.6 schema:alternateName School of Computer Science, University of Birmingham, Edgbaston, B15 2TT, Birmingham, UK
    236 schema:name School of Computer Science, University of Birmingham, Edgbaston, B15 2TT, Birmingham, UK
    237 rdf:type schema:Organization
    238 grid-institutes:grid.7605.4 schema:alternateName Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera 185, 10149, Torino, Italy
    239 schema:name Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera 185, 10149, Torino, Italy
    240 rdf:type schema:Organization
    241 grid-institutes:grid.8756.c schema:alternateName School of Computing Science, University of Glasgow, 18 Lilybank Gardens, G12 8RZ, Glasgow, Scotland, UK
    242 schema:name School of Computing Science, University of Glasgow, 18 Lilybank Gardens, G12 8RZ, Glasgow, Scotland, UK
    243 rdf:type schema:Organization
     




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


    ...