Reference : Number-Set Representations for Infinite-State Verification |

Scientific congresses and symposiums : Paper published in a book | |||

Engineering, computing & technology : Computer science | |||

http://hdl.handle.net/2268/74854 | |||

Number-Set Representations for Infinite-State Verification | |

English | |

Boigelot, Bernard [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >] | |

2006 | |

Proceedings of VISSAS 2005 | |

IOS Press | |

NATO Security through Science Series D: Information and Communication Security | |

1-16 | |

No | |

Yes | |

International | |

1-58603-570-3 | |

NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security (VISSAS 2005)" | |

March 2005 | |

Timisoara | |

Romania | |

[en] Infinite-state systems ; symbolic representations ; number-set representations | |

[en] In order to compute the reachability set of infinite-state models, one
needs a technique for exploring infinite sequences of transitions in finite time, as well as a symbolic representation for the finite and infinite sets of configurations that are to be handled. The representation problem can be solved by automata-based methods, which consist in representing a set by a finite-state machine recognizing its elements, suitably encoded as words over a finite alphabet. Automata-based set representations have many advantages: They are expressive, easy to manipulate, and admit a canonical form. In this survey, we describe two automata-based structures that have been developed for representing sets of numbers (or, more generally, of vectors): The Number Decision Diagram (NDD) for integer values, and the Real Vector Automaton (RVA) for real numbers. We discuss the expressiveness of these structures, present some construction algorithms, and give a brief introduction to some related acceleration techniques. | |

Researchers | |

http://hdl.handle.net/2268/74854 |

File(s) associated to this reference | ||||||||||||||

| ||||||||||||||

All documents in ORBi are protected by a user license.