About: LTL Model Checking of Parametric Timed Automata     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

AttributesValues
rdf:type
Description
  • The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The proposed problem could be solved using an explicit enumeration of all possible parameter valuations. However, we introduce a symbolic zone-based method for synthesising bounded integer parameters of parametric timed automata with an LTL specification. Our method extends the ideas of the standard automata-based approach to LTL model checking of timed automata. Our solution employs constrained parametric difference bound matrices and a suitable notion of extrapolation.
  • The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The proposed problem could be solved using an explicit enumeration of all possible parameter valuations. However, we introduce a symbolic zone-based method for synthesising bounded integer parameters of parametric timed automata with an LTL specification. Our method extends the ideas of the standard automata-based approach to LTL model checking of timed automata. Our solution employs constrained parametric difference bound matrices and a suitable notion of extrapolation. (en)
Title
  • LTL Model Checking of Parametric Timed Automata
  • LTL Model Checking of Parametric Timed Automata (en)
skos:prefLabel
  • LTL Model Checking of Parametric Timed Automata
  • LTL Model Checking of Parametric Timed Automata (en)
skos:notation
  • RIV/00216224:14330/14:00077081!RIV15-MSM-14330___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(EE2.3.30.0009), S
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 26727
http://linked.open...ai/riv/idVysledku
  • RIV/00216224:14330/14:00077081
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • Linear Temporal Logic; Parameter Synthesis; Parametric Timed Automata; Automata-based Model Checking (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [4471AE79CC49]
http://linked.open...v/mistoKonaniAkce
  • Telč, Czech Republic
http://linked.open...i/riv/mistoVydani
  • Brno, Czech Republic
http://linked.open...i/riv/nazevZdroje
  • MEMICS 2014
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Barnat, Jiří
  • Beneš, Nikola
  • Černá, Ivana
  • Bezděk, Peter
http://linked.open...vavai/riv/typAkce
http://linked.open.../riv/zahajeniAkce
number of pages
http://purl.org/ne...btex#hasPublisher
  • NOVPRESS
https://schema.org/isbn
  • 9788021450226
http://localhost/t...ganizacniJednotka
  • 14330
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software