Search results for "LTL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
90	Julien Groslambert	Verification of LTL on B Event Systems.	B	2007	DBLP DOI BibTeX RDF	Büchi Automaton, Verification, Refinement, LTL
81	Abigail Parisaca Vargas, Ana Gabriela Garis, Silvia Lizeth Tapia Tarifa, Chris George	Model Checking LTL Formulae in RAISE with FDR.	IFM	2009	DBLP DOI BibTeX RDF	model checking, formal methods, refinement, tools, CSP, LTL, FDR, RAISE, RSL
79	Rajeev Alur, Salvatore La Torre	Deterministic generators and games for Ltl fragments.	ACM Trans. Comput. Log.	2004	DBLP DOI BibTeX RDF	Games, Temporal Logic, Automata
73	Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi	Resets vs. Aborts in Linear Temporal Logic.	TACAS	2003	DBLP DOI BibTeX RDF
73	Klaus Havelund, Grigore Rosu	Monitoring Programs Using Rewriting.	ASE	2001	DBLP DOI BibTeX RDF
72	Salamah Salamah, Ann Q. Gates, Steve Roach	Improving Pattern-Based LTL Formulas for Automata Model Checking.	ITNG	2008	DBLP DOI BibTeX RDF	B¨uchi Automaton, Prospec, Composite Propositions, Pattern, LTL, Scope
71	Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila	Simple Is Better: Efficient Bounded Model Checking for Past LTL.	VMCAI	2005	DBLP DOI BibTeX RDF	Past LTL, Bounded Model Checking, NuSMV
70	Stéphane Demri, Ranko Lazic 0001, Arnaud Sangnier	Model Checking Freeze LTL over One-Counter Automata.	FoSSaCS	2008	DBLP DOI BibTeX RDF
70	Salamah Salamah, Ann Q. Gates, Steve Roach, Oscar Mondragon	Verifying Pattern-Generated LTL Formulas: A Case Study.	SPIN	2005	DBLP DOI BibTeX RDF
64	Norihiro Kamide	Embedding Linear-Time Temporal Logic into Infinitary Logic: Application to Cut-Elimination for Multi-agent Infinitary Epistemic Linear-Time Temporal Logic.	CLIMA	2008	DBLP DOI BibTeX RDF
61	Kristin Y. Rozier, Moshe Y. Vardi	LTL Satisfiability Checking.	SPIN	2007	DBLP DOI BibTeX RDF
61	Carsten Fritz	Concepts of Automata Construction from LTL.	LPAR	2005	DBLP DOI BibTeX RDF
61	Antonín Kucera 0001, Jan Strejcek	Characteristic Patterns for LTL.	SOFSEM	2005	DBLP DOI BibTeX RDF
61	Parosh Aziz Abdulla, Bengt Jonsson 0001, Marcus Nilsson, Julien d'Orso, Mayank Saksena	Regular Model Checking for LTL(MSO).	CAV	2004	DBLP DOI BibTeX RDF
61	Steven Eker, José Meseguer 0001, Ambarish Sridharanarayanan	The Maude LTL Model Checker and Its Implementation.	SPIN	2003	DBLP DOI BibTeX RDF
61	Frank D. Valencia	Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL.	ICLP	2003	DBLP DOI BibTeX RDF
61	Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi	Another Look at LTL Model Checking.	CAV	1994	DBLP DOI BibTeX RDF	model checking, temporal logic, binary decision diagrams, automatic verification
57	Julien Groslambert	A.	B	2007	DBLP DOI BibTeX RDF	Büchi Automaton, Verification, LTL
55	Orna Kupferman, Nir Piterman, Moshe Y. Vardi	From liveness to promptness.	Formal Methods Syst. Des.	2009	DBLP DOI BibTeX RDF	Verification, Temporal logic, Liveness
55	Orna Kupferman, Nir Piterman, Moshe Y. Vardi	From Liveness to Promptness.	CAV	2007	DBLP DOI BibTeX RDF
55	Francesco Ranzato, Francesco Tapparo	An Abstract Interpretation Perspective on Linear vs. Branching Time.	APLAS	2005	DBLP DOI BibTeX RDF
55	Zhiming Liu 0001, Anders P. Ravn, Xiaoshan Li	Unifying proof methodologies of duration calculus and timed linear temporal logic.	Formal Aspects Comput.	2004	DBLP DOI BibTeX RDF	Design, Verification, Real-time, Specification, Refinement
55	Marco Pistore, Moshe Y. Vardi	The Planning Spectrum - One, Two, Three, Infinity.	LICS	2003	DBLP DOI BibTeX RDF
53	Hans Svensson	Implementing an LTL-to-Büchi translator in Erlang: a protest experience report.	Erlang Workshop	2009	DBLP DOI BibTeX RDF	LTL-to-B?chi translator, QuickCheck, property driven development
53	Jiri Barnat, Ivana Cerná	Distributed breadth-first search LTL model checking.	Formal Methods Syst. Des.	2006	DBLP DOI BibTeX RDF	LTL model checking, Distributed memory, Breadth-first search
52	Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek	On decidability of LTL model checking for process rewrite systems.	Acta Informatica	2009	DBLP DOI BibTeX RDF
52	Nikola Benes, Lubos Brim, Ivana Cerná, Jiri Sochor, Pavlína Vareková, Barbora Zimmerová	Partial Order Reduction for State/Event LTL.	IFM	2009	DBLP DOI BibTeX RDF
52	Mikolaj Bojanczyk	The Common Fragment of ACTL and LTL.	FoSSaCS	2008	DBLP DOI BibTeX RDF
52	Martin De Wulf, Laurent Doyen 0001, Nicolas Maquet, Jean-François Raskin	Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking.	TACAS	2008	DBLP DOI BibTeX RDF
52	Andreas Morgenstern, Klaus Schneider 0001	From LTL to Symbolically Represented Deterministic Automata.	VMCAI	2008	DBLP DOI BibTeX RDF
52	Stéphane Demri, Ranko Lazic 0001	LTL with the Freeze Quantifier and Register Automata.	LICS	2006	DBLP DOI BibTeX RDF
52	Thomas Tuerk, Klaus Schneider 0001	From PSL to LTL: A Formal Validation in HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
52	Yulin Ding, Yan Zhang 0003	A Logic Approach for LTL System Modification.	ISMIS	2005	DBLP DOI BibTeX RDF	belief revision and update, model checking, temporal reasoning, Logic for Artificial Intelligence, model update
52	Mihalis Yannakakis, Kousha Etessami	Checking LTL Properties of Recursive Markov Chains.	QEST	2005	DBLP DOI BibTeX RDF
52	Stéphane Demri, Ranko Lazic 0001, David Nowak	On the Freeze Quantifier in Constraint LTL: Decidability and Complexity.	TIME	2005	DBLP DOI BibTeX RDF
52	Stéphane Demri	LTL over Integer Periodicity Constraints: (Extended Abstract).	FoSSaCS	2004	DBLP DOI BibTeX RDF
52	Howard Barringer, Allen Goldberg, Klaus Havelund, Koushik Sen	Program Monitoring with LTL in EAGLE.	IPDPS	2004	DBLP DOI BibTeX RDF
52	Antonín Kucera 0001, Jan Strejcek	The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL.	CSL	2002	DBLP DOI BibTeX RDF
52	Benedikt Bollig, Martin Leucker	Deciding LTL over Mazurkiewicz Traces.	TIME	2001	DBLP DOI BibTeX RDF
48	Malay K. Ganai, Aarti Gupta, Pranav Ashar	Beyond safety: customized SAT-based model checking.	DAC	2005	DBLP DOI BibTeX RDF	circuit cofactoring, unbounded model checking, formal verification, SAT, liveness, bounded model checking, LTL
47	Olga Kouchnarenko, Arnaud Lanoix	How to Verify and Exploit a Refinement of Component-Based Systems.	Ershov Memorial Conference	2006	DBLP DOI BibTeX RDF	LTL properties, verification, composition, refinement, modules, component-based systems
46	Ji Zhang, Heather Goldsby, Betty H. C. Cheng	Modular verification of dynamically adaptive systems.	AOSD	2009	DBLP DOI BibTeX RDF	global invariants, modular model checking, reliability, verification, formal specification, autonomic computing, dynamic adaptation
46	Sylvain Hallé, Roger Villemaire	XML Methods for Validation of Temporal Properties on Message Traces with Data.	OTM Conferences (1)	2008	DBLP DOI BibTeX RDF
46	Sertac Karaman, Ricardo G. Sanfelice, Emilio Frazzoli	Optimal control of Mixed Logical Dynamical systems with Linear Temporal Logic specifications.	CDC	2008	DBLP DOI BibTeX RDF
46	Vladimir V. Rybakov	Linear Temporal Logic with Until and Before on Integer Numbers, Deciding Algorithms.	CSR	2006	DBLP DOI BibTeX RDF	consecutions, admissible rules, algorithms, inference rules, linear temporal logic, logic in computer science, logical consequence
46	Andreas Bauer 0002, Martin Leucker, Christian Schallhart	Monitoring of Real-Time Properties.	FSTTCS	2006	DBLP DOI BibTeX RDF
46	Grigore Rosu, Klaus Havelund	Rewriting-Based Techniques for Runtime Verification.	Autom. Softw. Eng.	2005	DBLP DOI BibTeX RDF	verification, rewriting, runtime analysis
46	Dimitrie O. Paun, Marsha Chechik	Events in Linear-Time Properties.	RE	1999	DBLP DOI BibTeX RDF
45	Raphaël Khoury, Sylvain Hallé	Tally Keeping-LTL: An LTL Semantics for Quantitative Evaluation of LTL Specifications.	IRI	2018	DBLP DOI BibTeX RDF
45	Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila	Simple Bounded LTL Model Checking.	FMCAD	2004	DBLP DOI BibTeX RDF	linear translation, bounded model checking, LTL, NuSMV
45	Timo Latvala	Model Checking LTL Properties of High-Level Petri Nets with Fairness Constraints.	ICATPN	2001	DBLP DOI BibTeX RDF	Model checking, fairness, high-level Petri Nets, LTL
42	Jiri Barnat, Lubos Brim, Petr Rockai	A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties.	ICFEM	2009	DBLP DOI BibTeX RDF
42	Alexander Schimpf, Stephan Merz, Jan-Georg Smaus	Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
42	Min Wu, Gangfeng Yan, Zhiyun Lin, Ying Lan	Synthesis of output feedback control for motion planning based on LTL specifications.	IROS	2009	DBLP DOI BibTeX RDF
42	Patrice Godefroid, Nir Piterman	LTL Generalized Model Checking Revisited.	VMCAI	2009	DBLP DOI BibTeX RDF
42	Saqib Sohail, Fabio Somenzi, Kavita Ravi	A Hybrid Algorithm for LTL Games.	VMCAI	2008	DBLP DOI BibTeX RDF
42	Salamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach	Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications.	ATVA	2007	DBLP DOI BibTeX RDF
42	Manuel Clavel, Francisco Durán 0001, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer 0001, Carolyn L. Talcott	LTL Model Checking.	All About Maude	2007	DBLP DOI BibTeX RDF
42	Conghua Zhou, Shiguang Ju	SAT-based Bounded Model Checking for SE-LTL.	SNPD (3)	2007	DBLP DOI BibTeX RDF
42	Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek	On Decidability of LTL Model Checking for Process Rewrite Systems.	FSTTCS	2006	DBLP DOI BibTeX RDF
42	Moritz Hammer, Alexander Knapp, Stephan Merz	Truly On-the-Fly LTL Model Checking.	TACAS	2005	DBLP DOI BibTeX RDF
42	Viktor Schuppan, Armin Biere	Shortest Counterexamples for Symbolic Model Checking of LTL with Past.	TACAS	2005	DBLP DOI BibTeX RDF
42	Marko Samer, Helmut Veith	A Syntactic Characterization of Distributive LTL Queries.	ICALP	2004	DBLP DOI BibTeX RDF
42	Patrick Maier 0001	Intuitionistic LTL and a New Characterization of Safety and Liveness.	CSL	2004	DBLP DOI BibTeX RDF
42	Jean-Michel Couvreur, Nasser Saheb, Grégoire Sutre	An Optimal Automata Approach to LTL Model Checking of Probabilistic Systems.	LPAR	2003	DBLP DOI BibTeX RDF
42	Paulo Tabuada, George J. Pappas	Model Checking LTL over Controllable Linear Systems Is Decidable.	HSCC	2003	DBLP DOI BibTeX RDF
42	Heikki Tauriainen, Keijo Heljanko	Testing LTL formula translation into Büchi automata.	Int. J. Softw. Tools Technol. Transf.	2002	DBLP DOI BibTeX RDF	Model checking, Verification, Software testing, Temporal logic
42	Jerzy Marcinkowski, Tomasz Truderung	Optimal Complexity Bounds for Positive LTL Games.	CSL	2002	DBLP DOI BibTeX RDF
39	Wei Wang 0062, Dongyao Ji	Using SPIN to Detect Vulnerabilities in the AACS Drive-Host Authentication Protocol.	FORTE	2008	DBLP DOI BibTeX RDF	AACS, Authenticity, SPIN, LTL, Collusion Attack, Model Checker
39	Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar	Model Checking with Strong Fairness.	Formal Methods Syst. Des.	2006	DBLP DOI BibTeX RDF	fair discrete systems, temporal testers, model checking, temporal logic, fairness, CTL, LTL
39	Khalil Ajami, Serge Haddad, Jean-Michel Ilié	Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond.	TACAS	1998	DBLP DOI BibTeX RDF	Büchi automata, Model Checking, Verification, Temporal Logic, Symmetries, LTL
37	Sylvain Hallé, Roger Villemaire	Runtime monitoring of web service choreographies using streaming XML.	SAC	2009	DBLP DOI BibTeX RDF	streaming XML, web services, runtime monitoring
37	Clemens Ley, Michael Benedikt	How big must complete XML query languages be?	ICDT	2009	DBLP DOI BibTeX RDF
37	Franz Baader, Andreas Bauer 0002, Marcel Lippmann	Runtime Verification Using a Temporal Description Logic.	FroCoS	2009	DBLP DOI BibTeX RDF
37	Amanda M. Whitbrook, Uwe Aickelin, Jonathan M. Garibaldi	An Idiotypic Immune Network as a Short-Term Learning Architecture for Mobile Robots.	ICARIS	2008	DBLP DOI BibTeX RDF
37	Martin De Wulf, Laurent Doyen 0001, Nicolas Maquet, Jean-François Raskin	Alaska.	ATVA	2008	DBLP DOI BibTeX RDF
37	Marta Cialdea Mayer, Carla Limongelli, Andrea Orlandini, Valentina Poggioni	Linear temporal logic as an executable semantics for planning languages.	J. Log. Lang. Inf.	2007	DBLP DOI BibTeX RDF	Applied temporal logic, Knowledge representation, Artificial intelligence planning
37	Marius Kloetzer, Calin Belta	Managing non-determinism in symbolic robot motion planning and control.	ICRA	2007	DBLP DOI BibTeX RDF
37	Hadas Kress-Gazit, Georgios E. Fainekos, George J. Pappas	From structured english to robot motion.	IROS	2007	DBLP DOI BibTeX RDF
37	Zhilin Wu	On the Expressive Power of QLTL.	ICTAC	2007	DBLP DOI BibTeX RDF
37	Antonín Kucera 0001, Jan Strejcek	The stuttering principle revisited.	Acta Informatica	2005	DBLP DOI BibTeX RDF
37	Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman	Computational challenges in bounded model checking.	Int. J. Softw. Tools Technol. Transf.	2005	DBLP DOI BibTeX RDF	Bonded-Model-checking, Completeness-Threshold, Complexity
37	Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman	Completeness and Complexity of Bounded Model Checking.	VMCAI	2004	DBLP DOI BibTeX RDF
37	Dimitra Giannakopoulou, Klaus Havelund	Automata-Based Verification of Temporal Properties on Running Programs.	ASE	2001	DBLP DOI BibTeX RDF
37	Kousha Etessami	Stutter-Invariant Languages, omega-Automata, and Temporal Logic.	CAV	1999	DBLP DOI BibTeX RDF
37	Roderick Bloem, Kavita Ravi, Fabio Somenzi	Efficient Decision Procedures for Model Checking of Linear Time Logic Properties.	CAV	1999	DBLP DOI BibTeX RDF
37	Serenella Cerrito, Marta Cialdea Mayer	Using Linear Temporal Logic to Model and Solve Planning Problems.	AIMSA	1998	DBLP DOI BibTeX RDF	Planning, Temporal Reasoning, Linear Temporal Logic, Tableaux, Model Search
37	Moshe Y. Vardi	Sometimes and Not Never Re-revisited: On Branching Versus Linear Time.	CONCUR	1998	DBLP DOI BibTeX RDF
37	P. S. Thiagarajan, Igor Walukiewicz	An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces.	LICS	1997	DBLP DOI BibTeX RDF
35	Cuauhtemoc Munoz, Steve Roach	Automated Testing of LTL Formula Generation by Prospec.	HASE	2010	DBLP DOI BibTeX RDF	Prospec, Specification Pattern System, automated testing, LTL
35	Jiri Barnat, Lubos Brim, Pavel Simecek	Cluster-Based I/O-Efficient LTL Model Checking.	ASE	2009	DBLP DOI BibTeX RDF	I/O-efficient model checking, parallel model checking, LTL
35	Monika Maidl	The Common Fragment of CTL and LTL.	FOCS	2000	DBLP DOI BibTeX RDF	action-based computation tree logic, linear time logic, common fragment, ACTL formulas, PSPACE-complete problem, path quantifiers, 1-weak Buchi automaton, automaton size, formula size, computational complexity, temporal logic, trees (mathematics), decidability, finite automata, expressive power, negation, CTL, LTL, inductive definition
34	Fei Pu, Wenhui Zhang	Combining search space partition and abstraction for LTL model checking.	Sci. China Ser. F Inf. Sci.	2007	DBLP DOI BibTeX RDF	search space partition, LTL model checking, refinement, abstraction
34	Gordon Fraser 0001, Franz Wotawa	Using LTL rewriting to improve the performance of model-checker based test-case generation.	A-MOST	2007	DBLP DOI BibTeX RDF	LTL rewriting, test-case generation with model-checkers, automated software testing
34	Eric Bodden	A lightweight LTL runtime verification tool for java.	OOPSLA Companion	2004	DBLP DOI BibTeX RDF	joinpoints, linear-time temporal logic (LTL), metadata, aspectJ, concurrent systems, runtime verification
33	Emmanuel Filiot, Naiyong Jin, Jean-François Raskin	An Antichain Algorithm for LTL Realizability.	CAV	2009	DBLP DOI BibTeX RDF
33	Taolue Chen, Tingting Han 0001, Joost-Pieter Katoen, Alexandru Mereacre	LTL Model Checking of Time-Inhomogeneous Markov Chains.	ATVA	2009	DBLP DOI BibTeX RDF
33	Geng-Dian Huang, Lin-Zan Cai, Farn Wang	LTL Model Checking for Recursive Programs.	ATVA	2009	DBLP DOI BibTeX RDF
33	Bernd Finkbeiner, Lars Kuhtz	Monitor Circuits for LTL with Bounded and Unbounded Future.	RV	2009	DBLP DOI BibTeX RDF
33	Stefan Edelkamp, Peter Sanders 0001, Pavel Simecek	Semi-external LTL Model Checking.	CAV	2008	DBLP DOI BibTeX RDF