Branching data structures for real-time model checking not as good as thought

Clock Difference Diagrams (CDDs), BDD-like data structures for model checking of timed automata, were presented as alternatives for classic DBM representation. However, work on them seems to have stopped, although there are still important open questions. CDD definition required that repeated subtre...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Pérez, Gervasio, Pavese, Esteban, Schapachnik, Fernando
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 2012
Materias:
Ciencias Informáticas
Model Checking
Real-Time
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/123894
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-123894
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Model Checking
Real-Time
spellingShingle Ciencias Informáticas
Model Checking
Real-Time
Pérez, Gervasio
Pavese, Esteban
Schapachnik, Fernando
Branching data structures for real-time model checking not as good as thought
topic_facet Ciencias Informáticas
Model Checking
Real-Time
description Clock Difference Diagrams (CDDs), BDD-like data structures for model checking of timed automata, were presented as alternatives for classic DBM representation. However, work on them seems to have stopped, although there are still important open questions. CDD definition required that repeated subtrees were aliased, but no clear algorithm was presented for producing such compact representation, which seems costly to achieve. In this article we describe our implementation of such aliased subtrees and revisit CDDs by comparing their performance against DBMs on current case studies, with and without repeated subtrees. Our experiments show that CDDs still require more time and memory than DBMs, suggesting that eliminating repetitions is still not enough. Thus, this article re-opens issues that previous work on the topic considered closed.
format Objeto de conferencia
Objeto de conferencia
author Pérez, Gervasio
Pavese, Esteban
Schapachnik, Fernando
author_facet Pérez, Gervasio
Pavese, Esteban
Schapachnik, Fernando
author_sort Pérez, Gervasio
title Branching data structures for real-time model checking not as good as thought
title_short Branching data structures for real-time model checking not as good as thought
title_full Branching data structures for real-time model checking not as good as thought
title_fullStr Branching data structures for real-time model checking not as good as thought
title_full_unstemmed Branching data structures for real-time model checking not as good as thought
title_sort branching data structures for real-time model checking not as good as thought
publishDate 2012
url http://sedici.unlp.edu.ar/handle/10915/123894
work_keys_str_mv AT perezgervasio branchingdatastructuresforrealtimemodelcheckingnotasgoodasthought
AT paveseesteban branchingdatastructuresforrealtimemodelcheckingnotasgoodasthought
AT schapachnikfernando branchingdatastructuresforrealtimemodelcheckingnotasgoodasthought
bdutipo_str Repositorios
_version_ 1764820450465021953

Ejemplares similares