Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

1993

AUTHORS

Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger , Pei -Hsin Ho

ABSTRACT

We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties. More... »

PAGES

209-229

Book

TITLE

Hybrid Systems

ISBN

978-3-540-57318-0
978-3-540-48060-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/3-540-57318-6_30

DOI

http://dx.doi.org/10.1007/3-540-57318-6_30

DIMENSIONS

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


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/0101", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Pure Mathematics", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/01", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Mathematical Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Nokia (United States)", 
          "id": "https://www.grid.ac/institutes/grid.469490.6", 
          "name": [
            "AT&T Bell Laboratories, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Alur", 
        "givenName": "Rajeev", 
        "id": "sg:person.013634603172.55", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013634603172.55"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Crete", 
          "id": "https://www.grid.ac/institutes/grid.8127.c", 
          "name": [
            "Department of Computer Science, University of Crete, Greece"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Courcoubetis", 
        "givenName": "Costas", 
        "id": "sg:person.013765527421.82", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013765527421.82"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Cornell University", 
          "id": "https://www.grid.ac/institutes/grid.5386.8", 
          "name": [
            "Department of Computer Science, Cornell University, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Henzinger", 
        "givenName": "Thomas A.", 
        "id": "sg:person.010473344361.55", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010473344361.55"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Cornell University", 
          "id": "https://www.grid.ac/institutes/grid.5386.8", 
          "name": [
            "Department of Computer Science, Cornell University, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ho", 
        "givenName": "Pei -Hsin", 
        "id": "sg:person.010160737075.47", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010160737075.47"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "1993", 
    "datePublishedReg": "1993-01-01", 
    "description": "We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties.", 
    "editor": [
      {
        "familyName": "Grossman", 
        "givenName": "Robert L.", 
        "type": "Person"
      }, 
      {
        "familyName": "Nerode", 
        "givenName": "Anil", 
        "type": "Person"
      }, 
      {
        "familyName": "Ravn", 
        "givenName": "Anders P.", 
        "type": "Person"
      }, 
      {
        "familyName": "Rischel", 
        "givenName": "Hans", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/3-540-57318-6_30", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-57318-0", 
        "978-3-540-48060-0"
      ], 
      "name": "Hybrid Systems", 
      "type": "Book"
    }, 
    "name": "Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems", 
    "pagination": "209-229", 
    "productId": [
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/3-540-57318-6_30"
        ]
      }, 
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "c7a6ee3a63c9467a81368a68d10e96d0cd67573012749eab315009da408fb9ec"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1041912375"
        ]
      }
    ], 
    "publisher": {
      "location": "Berlin, Heidelberg", 
      "name": "Springer Berlin Heidelberg", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/3-540-57318-6_30", 
      "https://app.dimensions.ai/details/publication/pub.1041912375"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2019-04-15T17: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/0000000001_0000000264/records_8681_00000072.jsonl", 
    "type": "Chapter", 
    "url": "http://link.springer.com/10.1007/3-540-57318-6_30"
  }
]
 

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-57318-6_30'

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-57318-6_30'

Turtle is a human-readable linked data format.

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

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-57318-6_30'


 

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

107 TRIPLES      22 PREDICATES      27 URIs      20 LITERALS      8 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/3-540-57318-6_30 schema:about anzsrc-for:01
2 anzsrc-for:0101
3 schema:author N98fa994a0f9a460091cb96ee5eda1ff9
4 schema:datePublished 1993
5 schema:datePublishedReg 1993-01-01
6 schema:description We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties.
7 schema:editor N88aea5d9fba845fabcee2951623a7d64
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N3e96ee04530e455e8b17d4c3a568af0b
12 schema:name Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems
13 schema:pagination 209-229
14 schema:productId N3903b14d7a5b4a599ae40df672e9b83c
15 N84919cca594d4d27bbd6b2036a79baca
16 Ndd0254525ad646c8b1b1c6d95fc551cb
17 schema:publisher N6809d89dd6d84e8cacee3868860ff2a6
18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1041912375
19 https://doi.org/10.1007/3-540-57318-6_30
20 schema:sdDatePublished 2019-04-15T17:59
21 schema:sdLicense https://scigraph.springernature.com/explorer/license/
22 schema:sdPublisher Nfb79fbeea60a4879962348f7ef966fbf
23 schema:url http://link.springer.com/10.1007/3-540-57318-6_30
24 sgo:license sg:explorer/license/
25 sgo:sdDataset chapters
26 rdf:type schema:Chapter
27 N232ef57df3f345138f5f366fdb2d7c0e rdf:first sg:person.013765527421.82
28 rdf:rest N33278ada00ad470ab9f3df7c57b99283
29 N33278ada00ad470ab9f3df7c57b99283 rdf:first sg:person.010473344361.55
30 rdf:rest N3576e6b3955c406c80f6c50b658091c5
31 N3576e6b3955c406c80f6c50b658091c5 rdf:first sg:person.010160737075.47
32 rdf:rest rdf:nil
33 N3903b14d7a5b4a599ae40df672e9b83c schema:name readcube_id
34 schema:value c7a6ee3a63c9467a81368a68d10e96d0cd67573012749eab315009da408fb9ec
35 rdf:type schema:PropertyValue
36 N3cf608aeaca641aba95dfd815f6f8412 rdf:first Ne735cc756c8a460aadda5d3490ea750a
37 rdf:rest rdf:nil
38 N3e96ee04530e455e8b17d4c3a568af0b schema:isbn 978-3-540-48060-0
39 978-3-540-57318-0
40 schema:name Hybrid Systems
41 rdf:type schema:Book
42 N4fdabcab254449569a706e7b6f29ea07 schema:familyName Ravn
43 schema:givenName Anders P.
44 rdf:type schema:Person
45 N605be54ebf44406f9e48ec2689c25ba3 rdf:first N4fdabcab254449569a706e7b6f29ea07
46 rdf:rest N3cf608aeaca641aba95dfd815f6f8412
47 N6809d89dd6d84e8cacee3868860ff2a6 schema:location Berlin, Heidelberg
48 schema:name Springer Berlin Heidelberg
49 rdf:type schema:Organisation
50 N7e4bd93d286d45ce8353e111c69490b6 schema:familyName Grossman
51 schema:givenName Robert L.
52 rdf:type schema:Person
53 N84919cca594d4d27bbd6b2036a79baca schema:name doi
54 schema:value 10.1007/3-540-57318-6_30
55 rdf:type schema:PropertyValue
56 N88aea5d9fba845fabcee2951623a7d64 rdf:first N7e4bd93d286d45ce8353e111c69490b6
57 rdf:rest Nfa525bcc31cd4266bc0f4833388d77c6
58 N98fa994a0f9a460091cb96ee5eda1ff9 rdf:first sg:person.013634603172.55
59 rdf:rest N232ef57df3f345138f5f366fdb2d7c0e
60 Nab264e5426734f6aab0ab929988be463 schema:familyName Nerode
61 schema:givenName Anil
62 rdf:type schema:Person
63 Ndd0254525ad646c8b1b1c6d95fc551cb schema:name dimensions_id
64 schema:value pub.1041912375
65 rdf:type schema:PropertyValue
66 Ne735cc756c8a460aadda5d3490ea750a schema:familyName Rischel
67 schema:givenName Hans
68 rdf:type schema:Person
69 Nfa525bcc31cd4266bc0f4833388d77c6 rdf:first Nab264e5426734f6aab0ab929988be463
70 rdf:rest N605be54ebf44406f9e48ec2689c25ba3
71 Nfb79fbeea60a4879962348f7ef966fbf schema:name Springer Nature - SN SciGraph project
72 rdf:type schema:Organization
73 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
74 schema:name Mathematical Sciences
75 rdf:type schema:DefinedTerm
76 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
77 schema:name Pure Mathematics
78 rdf:type schema:DefinedTerm
79 sg:person.010160737075.47 schema:affiliation https://www.grid.ac/institutes/grid.5386.8
80 schema:familyName Ho
81 schema:givenName Pei -Hsin
82 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010160737075.47
83 rdf:type schema:Person
84 sg:person.010473344361.55 schema:affiliation https://www.grid.ac/institutes/grid.5386.8
85 schema:familyName Henzinger
86 schema:givenName Thomas A.
87 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010473344361.55
88 rdf:type schema:Person
89 sg:person.013634603172.55 schema:affiliation https://www.grid.ac/institutes/grid.469490.6
90 schema:familyName Alur
91 schema:givenName Rajeev
92 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013634603172.55
93 rdf:type schema:Person
94 sg:person.013765527421.82 schema:affiliation https://www.grid.ac/institutes/grid.8127.c
95 schema:familyName Courcoubetis
96 schema:givenName Costas
97 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013765527421.82
98 rdf:type schema:Person
99 https://www.grid.ac/institutes/grid.469490.6 schema:alternateName Nokia (United States)
100 schema:name AT&T Bell Laboratories, USA
101 rdf:type schema:Organization
102 https://www.grid.ac/institutes/grid.5386.8 schema:alternateName Cornell University
103 schema:name Department of Computer Science, Cornell University, USA
104 rdf:type schema:Organization
105 https://www.grid.ac/institutes/grid.8127.c schema:alternateName University of Crete
106 schema:name Department of Computer Science, University of Crete, Greece
107 rdf:type schema:Organization
 




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


...