Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Tối thiểu hóa không gian trạng thái phân tán
Tóm tắt
Chúng tôi trình bày một thuật toán mới, cùng với thực thi phân tán của nó, nhằm giảm thiểu các hệ thống chuyển tiếp có nhãn theo mô-đun đồng đồng nhất mạnh. Cơ sở của thuật toán này là "phương pháp ngây thơ" của Kanellakis–Smolka, mặc dù có độ phức tạp lý thuyết cao nhưng lại thành công trong thực tiễn và rất thích hợp với việc song song hóa. Phương pháp cơ bản này được kết hợp với các tối ưu hóa dựa trên thuật toán Kanellakis–Smolka cho trường hợp số đầu ra giới hạn, vốn có độ phức tạp thời gian tốt nhất được biết đến. Thực thi phân tán được cải thiện so với những nỗ lực trước đó nhờ vào việc chồng chéo tốt hơn giữa giao tiếp và tính toán, dẫn đến việc sử dụng hiệu quả cả bộ nhớ và công suất xử lý. Chúng tôi cũng thảo luận về độ phức tạp thời gian của thuật toán này và trình bày các kết quả thực nghiệm với các công cụ mẫu tuần tự và phân tán.
Từ khóa
#thuật toán #thực thi phân tán #giảm thiểu hệ thống chuyển tiếp #đồng đồng nhất mạnh #Kanellakis–Smolka #tối ưu hóa #phức tạp thời gianTài liệu tham khảo
Barnat J, Brim L, Stříbrná J (2001) Distributed LTL model-checking in SPIN. In: Proceedings SPIN’01. Lecture notes in computer science, vol 2057. Springer, Berlin Heidelberg New York, pp 200–216
Behrmann G, Hune T, Vaandrager FW (2000) Distributed timed model checking – how the search order matters. In: Proceedings CAV’00. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 216–231
Berry G, Comon H, Finkel A (eds) (2001) Proceedings CAV’01. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York
Blom SCC, Fokkink WJ, Groote JF, van Langevelde I, Lisser B, van de Pol JC (2001) μCRL: a toolset for analysing algebraic specifications. In: Proceedings CAV’01. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 250–254
Blom SCC, Orzan SM (2002) A distributed algorithm for strong bisimulation reduction of state spaces. In: Proceedings PDMC’02. Electronic notes in theoretical computer science, vol 68
CWI/SEN2, INRIA/VASY. The VLTS benchmark. http://www.inrialpes.fr/vasy/cadp/resources/benchmark_bcg.html
Fernandez J-C, Mounier L (1990) Verifying bisimulations “on the fly”. In: Proceedings FORTE’90
Garavel H, Mounier L (1997) Specification and verification of various distributed leader election algorithms for unidirection ring networks. Sci Comput Programm 29(1–2):171–197
van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3):555–600
Groote JF, Pang J, Wouters AG (2003) Analyzing a distributed system for lifting trucks. J Logic Algebr Programm 55(1–2):21–56
Grumberg O, Heyman T, Schuster A (2001) Distributed symbolic model checking for μ-calculus. In: Berry G, Comon H, Finkel A (eds) [3], pp 350–362
Hopcroft JE (1971) An n log n algorithm for minimizing the states in a finite automaton. In: The theory of machines and computations. Academic, New York, pp 189–196
Joubert C, Mateescu R (2004) Distributed on-the-fly equivalence checking. In: Proceedings PDMC’04. Electronic notes in theoretical computer science (in press)
Kanellakis PC, Smolka SA (1983) CCS expressions, finite state processes and three problems of equivalence. In: Proceedings 2nd annual ACM symposium on principles of distributed computing, pp 228–240
Lerda F, Sisto R (1999) Distributed-memory model checking with SPIN. In: Proceedings SPIN’00. Lecture notes in computer science, vol 1680. Springer, Berlin Heidelberg New York
Leucker M, Noll T (2001) Truth/SLC – a parallel verification platform for concurrent systems. In: Berry G, Comon H, Finkel A (eds) [3], pp 255–259
Luttik SP (1997) Description and formal specification of the Link Layer of P1394. In: Proceedings 2nd international workshop on applied formal methods in system design
Mateescu R (2003) A generic on-the-fly solver for alternation-free boolean equation systems. In: Proceedings TACAS’01. Lecture notes in computer science, vol 2619. Springer, Berlin Heidelberg New York, pp 81–96
Paige R, Tarjan R (1987) Three partition refinement algorithms. SIAM J Comput 16(6):973–989
Pang J, Fokkink WJ, Hofman R, Veldema R (2003) Model checking a cache coherence protocol for a Java DSM implementation. In: Proceedings FMPPTA’03
van de Pol JC, Valero Espada M (2003) Verification of JavaSpaces parallel programs. In: Proceedings ACSD’03, pp 196–205
Rajasekaran S, Lee I (1998) Parallel algorithms for relational coarsest partition problems. IEEE Trans Parallel Distrib Syst 9(7):687–699
Romijn JMT (2001) A timed verification of the ieee 1394 leader election protocol. Formal Methods Syst Des 19(2):165–194
Stern U, Dill D (1997) Parallelizing the Murφ verifier. In: Proceedings CAV’97. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 256–278
Zhang S, Smolka SA (1993) Towards efficient parallelization of equivalence checking algorithms. In: Proceedings FORTE’92. IFIP Trans C-10:133–146