About: On Clock-Aware LTL Properties of Timed Automata

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: On Clock-Aware LTL Properties of 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)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique. We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique. (en)
Title	On Clock-Aware LTL Properties of Timed Automata On Clock-Aware LTL Properties of Timed Automata (en)
skos:prefLabel	On Clock-Aware LTL Properties of Timed Automata On Clock-Aware LTL Properties of Timed Automata (en)
skos:notation	RIV/00216224:14330/14:00076564!RIV15-MSM-14330___
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(EE2.3.30.0009), P(LH11065)
http://linked.open...vai/riv/dodaniDat	2015
http://linked.open...aciTvurceVysledku	Bezděk, Peter Havel, Vojtěch Beneš, Nikola Černá, Ivana Barnat, Jiří
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	34250
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/14:00076564
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Linear Temporal Logic; Timed Automata; Automata-based Model Checking (en)
http://linked.open.../riv/klicoveSlovo	Automata-based Model Checking Linear Temporal Logic Timed Automata
http://linked.open...ontrolniKodProRIV	[AEE613D55B18]
http://linked.open...v/mistoKonaniAkce	Bucharest, Romania
http://linked.open...i/riv/mistoVydani	Neuveden
http://linked.open...i/riv/nazevZdroje	Theoretical Aspects of Computing – ICTAC 2014
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	5 (xsd:int)
http://linked.open...cetTvurcuVysledku	5 (xsd:int)
http://linked.open...vavai/riv/projekt	Control Synthesis and Formal Verification of Complex Hybrid Systems Employment of Newly Graduated Doctors of Science for Scientific Excellence
http://linked.open...UplatneniVysledku	2014
http://linked.open...iv/tvurceVysledku	Barnat, Jiří Beneš, Nikola Černá, Ivana Havel, Vojtěch Bezděk, Peter
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2014-01-01 (xsd:date)
issn	0302-9743
number of pages	18 (xsd:int)
http://bibframe.org/vocab/doi	10.1007/978-3-319-10882-7_4
http://purl.org/ne...btex#hasPublisher	Springer International Publishing
https://schema.org/isbn	9783319108810
http://localhost/t...ganizacniJednotka	14330

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

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, 112 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software