Deductive temporal reasoning with constraints

Abate, 2003, The Tableaux Workbench, vol. 2796, 230 O. Bailleux, Y. Boufkhad, Efficient CNF encoding of boolean cardinality constraints, in: Ninth International Conference on Principles and Practice of Constraint Programming (CP), in: LNCS, vol. 2833, pp. 108–122. Barringer, 1987, Up and down the temporal way, The Computer Journal, 30, 134, 10.1093/comjnl/30.2.134 Behdenna, 2009, Deductive verification of simple foraging robotic behaviours, International Journal of Intelligent Computing and Cybernetics, 2, 604, 10.1108/17563780911005818 Benhamou, 1994, Two proof procedures for a cardinality based language in propositional calculus, 71 Bordeaux, 2006, Propositional satisfiability and constraint programming: A comparative survey, ACM Computing Surveys, 38, 10.1145/1177352.1177354 Cheng, 1995, Complexity results for 1-safe nets, Theoretical Computer Science, 147, 117, 10.1016/0304-3975(94)00231-7 Chockler, 2011, Incremental formal verification of hardware, 125 A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV 2: An opensource tool for symbolic model checking, in: Proceedings of International Conference on Computer-Aided Verification (CAV), pp. 359–364. Clarke, 1981, Design and synthesis of synchronization skeletons using branching-time temporal logic, vol. 131, 52 Clarke, 1986, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, 8, 244, 10.1145/5397.5399 Clarke, 2000 Daniele, 1999, Improved automata generation for linear temporal logic, vol. 1633, 249 Davis, 1960, A computing procedure for quantification theory, Journal of the ACM, 7, 201, 10.1145/321033.321034 Davis, 1962, A machine program for theorem-proving, ACM Communications, 5, 394, 10.1145/368273.368557 Degtyarev, 2002, A simplified clausal resolution procedure for propositional linear-time temporal logic, vol. 2381, 85 Demri, 2002, The complexity of propositional linear temporal logics in simple cases, Information and Computation, 174, 84, 10.1006/inco.2001.3094 Dixon, 2006, Is there a future for deductive temporal verification?, 11 Dixon, 2007, Temporal logic with capacity constraints, vol. 4720, 163 Dixon, 2007, Tractable temporal reasoning, 318 C. Dixon, M. Fisher, B. Konev, Taming the complexity of temporal epistemic reasoning, in: Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS), LNAI, 2009, pp. 198–213. Esparza, 1996, Decidability and complexity of Petri net problems—an introduction, vol. 1491, 374 C.F. Fan, C.H. Sun, S. Yih, A dual language approach to software formal specifications and safety analysis, in: Proceedings of the 2002 International Computer Symposium (ICS), pp. 1126–1133. Fernández Gago, 2005, First-order verification in practice, Journal of Automated Reasoning, 34, 295, 10.1007/s10817-005-7354-1 Finger, 1993, METATEM at work: Modelling reactive systems using executable temporal logic, 209 Fisher, 1991, A resolution method for temporal logic, 99 Fisher, 2011 Fisher, 2006, Practical infinite-state verification with temporal reasoning, vol. 1, 91 Fisher, 2001, Clausal temporal resolution, ACM Transactions on Computational Logic, 2, 12, 10.1145/371282.371311 Flum, 2006 Gabbay, 1980, The temporal analysis of fairness, 163 Gent, 1994, The SAT phase transition, 105 Giannakopoulou, 2002, From states to transitions: Improving translation of LTL formulae to Büchi automata, vol. 2529, 308 G.D. Gough, Decision procedures for temporal logic, Masterʼs thesis, Department of Computer Science, University of Manchester, 1984, Also University of Manchester, Department of Computer, Science, Technical Report UMCS-89-10-1. Handy, 1993 Hinton, 2006, PRISM: A tool for automatic verification of probabilistic systems, vol. 3920, 441 Hoare, 1985 Holzmann, 2003 Hustadt, 2003, TRP++ 2.0: A temporal resolution prover, vol. 2741, 274 G. Jaeger, P. Balsiger, A. Heuerding, S. Schwendimann, M. Bianchi, K. Guggisberg, G. Janssen, W. Heinle, F. Achermann, A.D. Boroumand, P. Brambilla, I. Bucher, H. Zimmermann, LWB—The Logics Workbench 1.1, University of Berne, Switzerland, 2002, www.lwb.unibe.ch. G. Janssen, Logics for digital circuit verification—theory, algorithms, and applications, Ph.D. thesis, University of Eindhoven, 1999. Jones, 1977, Complexity of some problems in Petri nets, Theoretical Computer Science, 4, 277, 10.1016/0304-3975(77)90014-7 Lamport, 2003 Manna, 1992 J. Nembrini, Minimalist coherent swarming of wireless networked autonomous mobile robots, Ph.D. thesis, University of the West of England, 2005. Prasad, 2005, A survey of recent advances in SAT-based formal verification, International Journal on Software Tools for Technology Transfer, 7, 156, 10.1007/s10009-004-0183-4 Reif, 2004, Integrated formal methods for safety analysis and train systems, 637 Reisig, 1998 Russell, 2010 S. Schwendimann, Aspects of computational logic, Ph.D. thesis, Universität Bern, Switzerland, 1998. Sebastiani, 2005, Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking, vol. 3576, 350 Sinz, 2005, Towards an optimal CNF encoding of boolean cardinality constraints, vol. 3709, 827 Suda, 2012, Labelled superposition for PLTL Visser, 2003, Model checking programs, Automated Software Engineering, 10, 203, 10.1023/A:1022920129859 Walsh, 2000, SAT v CSP, vol. 1894, 441 Winfield, 2005, On formal specification of emergent behaviours in swarm robotic systems, International Journal of Advanced Robotic Systems, 2, 363, 10.5772/5769 Wolper, 1985, The tableau method for temporal logic: An overview, Logique et Analyse, 110–111, 119 Wood, 1989, Temporal logic case study, vol. 407, 257