BRIM, Luboš, Jitka CRHOVÁ and Karen YORAV. Using Assumptions to Distribute CTL Model Checking. Brno, Czech Republic, 2002, p. 1-22. Technical Report FIMU-RS-2002-08.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Using Assumptions to Distribute CTL Model Checking
Authors BRIM, Luboš, Jitka CRHOVÁ and Karen YORAV.
Edition Brno, Czech Republic, p. 1-22, Technical Report FIMU-RS-2002-08. 2002.
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 20206 Computer hardware and architecture
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
Organization unit Faculty of Informatics
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 22/11/2006 08:32.
Abstract
In this work we discuss the problem of performing distributed CTL model checking by splitting the given state space into several ``partial state spaces''. The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about the truth of formulas and the computers exchange assumptions about relevant states as they compute more precis
Links
GA201/00/1023, research and development projectName: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Czech Science Foundation, Algorithms and tools for practical verification of concurrent systems.
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
PrintDisplayed: 15/10/2024 16:55