SAT-Based Reachability Checking for Timed Automata with Discrete Data

• Autorzy: Zbrzezny A. , Półrola A.
• Języki publikacji: EN

Słowa kluczowe

EN

Timed Automata; reachability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 3-4
• Strony: 579--593
• Opis fizyczny: bibliogr. 19 poz., tab., wykr.

Twórcy

autor

Zbrzezny A.

autor

Półrola A.

• Institute of Mathematics and Computer Science, Jan Długosz University, Armii Krajowej 13/15, 42-200 Częstochowa, Poland,

Bibliografia

• [1] R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of the 17th Int. Colloquium on Automata, Languages and Programming (ICALP'90), volume 443 of LNCS, pages 322-335. Springer-Verlag, 1990.
• [2] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
• [3] G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani. Bounded model checking for timed systems. In Proc. of the 22nd Int. Conf. on Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of LNCS, pages 243-259. Springer-Verlag, 2002.
• [4] K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260-261, 1969.
• [5] G. Behrmann, K. G. Larsen, J. Pearson, C.Weise, andW. Yi. Efficient timed reachability analysis using Clock Difference Diagrams. In Proc. of the 11th Int. Conf. on Computer Aided Verification (CAV'99), volume 1633 of LNCS, pages 341-353. Springer-Verlag, 1999.
• [6] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of UPPAAL. In Proc. of the Int. Workshop on Software Tools for Technology Transfer, 1998.
• [7] J. Bengtsson and W. Yi. On clock difference constraints and termination in reachability analysis in timed automata. In Proc. of the 5th Int. Conf. on Formal Methods and Software Engineering (ICFEM'03), volume 2885 of LNCS, pages 491-503. Springer-Verlag, 2003.
• [8] D. Beyer. Improvements in BDD-based reachability analysis of timed automata. In Proc. of the Int. Symp. Formal Methods Europe (FME'01), volume 2021 of LNCS, pages 318-343. Springer-Verlag, 2002.
• [9] M. Bozga, O. Maler, and S. Tripakis. Efficient verification of timed automata using dense and discrete time semantics. In Proc. of the Conf. on Correct Hardware Design and Verification Methods (CHARME'99), volume 1703 of LNCS, pages 125-141. Springer-Verlag, 1999.
• [10] C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. Of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), volume 1384 of LNCS, pages 313-329. Springer-Verlag, 1998.
• [11] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerICS: A tool for verifying timed automata and Estelle specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [12] P. Merlin and D. J. Farber. Recoverability of communication protocols - implication of a theoretical study. IEEE Trans. on Communications, 24(9):1036-1043, 1976.
• [13] MiniSat. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat, 2006.
• [14] W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [15] A. Półrola, W. Penczek, and M. Szreter. Towards efficient partition refinement for checking reachability in timed automata. In Proc. of the 1st Int. Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS'03), volume 2791 of LNCS, pages 2-17. Springer-Verlag, 2004.
• [16] C. Ramchandani. Analysis of asynchronous concurrent systems by timed Petri nets. Technical ReportMACTR-120, Massachusetts Institute of Technology, February 1974.
• [17] B. Woźna, A. Zbrzezny, and W. Penczek. Checking reachability properties for timed automata via SAT. Fundamenta Informaticae, 55(2):223-241, 2003.
• [18] A. Zbrzezny. Improvements in SAT-based reachability analysis for timed automata. Fundamenta Informaticae, 60(1-4):417-434, 2004.
• [19] A. Zbrzezny. SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae, 67(1-3):303-322, 2005.