How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC and Jiří ŠIMŠA. How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005). Lisboa, Portugal: TU Munchen, 2005, p. 1-12.

Basic information

• Original name: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
• Name in Czech: Uspořádání vrcholů pro distribuované ověřování LTL vlastností modelu založené na akceptujících předchůdcích
• Authors: BRIM, Luboš (203 Czech Republic, guarantor), Ivana ČERNÁ (203 Czech Republic), Pavel MORAVEC (203 Czech Republic) and Jiří ŠIMŠA (203 Czech Republic).
• Edition: Lisboa, Portugal, Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005), p. 1-12, 2005.
• Publisher: TU Munchen

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Portugal
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/05:00012461
• Organization unit: Faculty of Informatics
• Keywords in English: accepting predecessors; LTL model checking
• Tags: accepting predecessors, LTL model checking
• Tags: International impact, Reviewed

Abstract

The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B\"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well.

Abstract (in Czech)

Článek zkoumá problém optimálního uspořádání dříve prezentovaného algoritmu pro distribuované ověřování LTL vlastností modelu a prezentuje několik heuristik pro nalezení optimálního uspořádání v distribuovaném prostředí.

Links

• GA201/03/0509, research and development project: Name: Automatizovaná verifikace paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems

• GD102/05/H050, research and development project: Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science