R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer & M. Vardi (2003):
Enhanced Vacuity Detection in Linear Temporal Logic.
In: W. Hunt Jr. & F. Somenzi: CAV,
LNCS 2725.
Springer,
pp. 368–380,
doi:10.1007/978-3-540-45069-6_35.
A. Awad, R. Goré, Z. Hou, J. Thomson & M. Weidlich (2012):
An iterative approach to synthesize business process templates from compliance rules.
Inf. Syst. 37(8),
pp. 714–736,
doi:10.1016/j.is.2012.05.001.
R. Bakker, F. Dikker, F. Tempelman & P. Wognum (1993):
Diagnosing and Solving Over-Determined Constraint Satisfaction Problems.
In: IJCAI,
pp. 276–281.
Available at http://ijcai.org/Past.
I. Beer, S. Ben-David, H. Chockler, A. Orni & R. Trefler (2009):
Explaining Counterexamples Using Causality.
In: A. Bouajjani & O. Maler: CAV,
LNCS 5643.
Springer,
pp. 94–108,
doi:10.1007/978-3-642-02658-4_11.
I. Beer, S. Ben-David, C. Eisner & Y. Rodeh (2001):
Efficient Detection of Vacuity in Temporal Model Checking.
FMSD 18(2),
pp. 141–163,
doi:10.1023/A:1008779610539.
A. Behdenna, C. Dixon & M. Fisher (2009):
Deductive Verification of Simple Foraging Robotic Behaviours.
Int. J. of Intelligent Comput. and Cybernetics 2(4),
pp. 604–643,
doi:10.1108/17563780911005818.
R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli & M. Weiglhofer (2007):
Specify, Compile, Run: Hardware from PSL.
In: S. Glesner, J. Knoop & R. Drechsler: COCV,
ENTCS 190(4).
Elsevier,
pp. 3–16,
doi:10.1016/j.entcs.2007.09.004.
A. Chiappini, A. Cimatti, L. Macchi, O. Rebollo, M. Roveri, A. Susi, S. Tonetta & B. Vittorini (2010):
Formalization and validation of a subset of the European Train Control System.
In: J. Kramer, J. Bishop, P. Devanbu & S. Uchitel: ICSE (2).
ACM,
pp. 109–118,
doi:10.1145/1810295.1810312.
E. Clarke, M. Talupur, H. Veith & D. Wang (2003):
SAT Based Predicate Abstraction for Hardware Verification.
In: E. Giunchiglia & A. Tacchella: SAT,
LNCS 2919.
Springer,
pp. 78–92,
doi:10.1007/978-3-540-24605-3_7.
C. Dixon (1997):
Using Otter for Temporal Resolution.
In: H. Barringer, M. Fisher, D. Gabbay & G. Gough: ICTL,
Applied Logic Series.
Kluwer,
pp. 149–166.
C. Dixon (1998):
Temporal Resolution Using a Breadth-First Search Algorithm.
Ann. Math. Artif. Intell. 22(1-2),
pp. 87–115,
doi:10.1023/A:1018942108420.
C. Eisner & D. Fisman (2006):
A Practical Introduction to PSL.
Springer,
doi:10.1007/978-0-387-36123-9.
E. Emerson (1990):
Temporal and Modal Logic.
In: J. van Leeuwen: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B).
Elsevier and MIT Press,
pp. 995–1072.
M. Fisher (1991):
A Resolution Method for Temporal Logic.
In: IJCAI,
pp. 99–104.
Available at http://ijcai.org/Past.
M. Fisher, C. Dixon & M. Peim (2001):
Clausal temporal resolution.
ACM Trans. Comput. Log. 2(1),
pp. 12–56,
doi:10.1145/371282.371311.
P. Gawrychowski (2011):
Chrobak Normal Form Revisited, with Applications.
In: B. Bouchou-Markhoff, P. Caron, J. Champarnaud & D. Maurel: CIAA,
LNCS 6807.
Springer,
pp. 142–153,
doi:10.1007/978-3-642-22256-6_14.
F. Hantry & M. Hacid (2011):
Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages.
In: E. Pimentel & V. Valero: FLACOS,
EPTCS 68,
pp. 39–53,
doi:10.4204/EPTCS.68.5.
A. Harding (2005):
Symbolic Strategy Synthesis For Games With LTL Winning Conditions.
University of Birmingham.
J. Hopcroft & J. Ullman (1979):
Introduction to Automata Theory, Languages and Computation.
Addison-Wesley.
U. Hustadt & B. Konev (2003):
TRP++ 2.0: A Temporal Resolution Prover.
In: F. Baader: CADE,
LNCS 2741.
Springer,
pp. 274–278,
doi:10.1007/978-3-540-45085-6_21.
U. Hustadt & B. Konev (2004):
TRP++: A temporal resolution prover.
In: M. Baaz, J. Makowsky & A. Voronkov: Collegium Logicum 8.
Kurt Gödel Society,
pp. 65–79.
U. Hustadt & R. A. Schmidt (2002):
Scientific Benchmarking with Temporal Logic Decision Procedures.
In: D. Fensel, F. Giunchiglia, D. McGuinness & M. Williams: KR.
Morgan Kaufmann,
pp. 533–546.
T. Jussila, C. Sinz & A. Biere (2006):
Extended Resolution Proofs for Symbolic SAT Solving with Quantification.
In: A. Biere & C. Gomes: SAT,
LNCS 4121.
Springer,
pp. 54–60,
doi:10.1007/11814948_8.
R. Parikh (1966):
On Context-Free Languages.
J. ACM 13(4),
pp. 570–581,
doi:10.1145/321356.321364.
M. Pesic & W. van der Aalst (2006):
A Declarative Approach for Flexible Business Processes Management.
In: J. Eder & S. Dustdar: Business Process Management Workshops,
LNCS 4103.
Springer,
pp. 169–180,
doi:10.1007/11837862_18.
I. Pill, S. Semprini, R. Cavada, M. Roveri, R. Bloem & A. Cimatti (2006):
Formal analysis of hardware requirements.
In: E. Sentovich: DAC.
ACM,
pp. 821–826,
doi:10.1145/1146909.1147119.
K. Ravi & F. Somenzi (2004):
Minimal Assignments for Bounded Model Checking.
In: K. Jensen & A. Podelski: TACAS,
LNCS 2988.
Springer,
pp. 31–45,
doi:10.1007/978-3-540-24730-2_3.
K. Rozier & M. Vardi (2010):
LTL satisfiability checking.
STTT 12(2),
pp. 123–137,
doi:10.1007/s10009-010-0140-3.
Z. Sawa (2013):
Efficient Construction of Semilinear Representations of Languages Accepted by Unary Nondeterministic Finite Automata.
Fundam. Inform. 123(1),
pp. 97–106,
doi:10.3233/FI-2013-802.
V. Schuppan (2012):
Extracting Unsatisfiable Cores for LTL via Temporal Resolution.
Available at http://arxiv.org/abs/1212.3884v1arXiv:1212.3884v1 [cs.LO].
V. Schuppan (2012):
Towards a notion of unsatisfiable and unrealizable cores for LTL.
Sci. Comput. Program. 77(7-8),
pp. 908–939,
doi:10.1016/j.scico.2010.11.004.
V. Schuppan & L. Darmawan (2011):
Evaluating LTL Satisfiability Solvers.
In: T. Bultan & P. Hsiung: ATVA,
LNCS 6996.
Springer,
pp. 397–413,
doi:10.1007/978-3-642-24372-1_28.
J. Simmonds, J. Davies, A. Gurfinkel & M. Chechik (2010):
Exploiting resolution proofs to speed up LTL vacuity detection for BMC.
STTT 12(5),
pp. 319–335,
doi:10.1007/s10009-009-0134-1.
M. De Wulf, L. Doyen, N. Maquet & J. Raskin (2008):
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking.
In: C. Ramakrishnan & J. Rehof: TACAS,
LNCS 4963.
Springer,
pp. 63–77,
doi:10.1007/978-3-540-78800-3_6.
eptcs@eptcs.org