Search results for "LTL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
33	Kais Klai, Denis Poitrenaud	MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs.	Petri Nets	2008	DBLP DOI BibTeX RDF
33	Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber	Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking.	TACAS	2008	DBLP DOI BibTeX RDF
33	Jiri Barnat, Lubos Brim, Petr Rockai	Scalable Multi-core LTL Model-Checking.	SPIN	2007	DBLP DOI BibTeX RDF
33	Juan Antonio Navarro Pérez, Andrei Voronkov	Encodings of Bounded LTL Model Checking in Effectively Propositional Logic.	CADE	2007	DBLP DOI BibTeX RDF
33	Stéphane Demri, Régis Gascon	The Effects of Bounding Syntactic Resources on Presburger LTL.	TIME	2007	DBLP DOI BibTeX RDF
33	Mohammed Al Achhab, Ahmed Hammad, Hassan Mountassir	Verifying LTL Properties on Hierarchical Systems: Application to Aircraft Autopilot.	ISoLA	2006	DBLP DOI BibTeX RDF
33	Alexandre Genon, Thierry Massart, Cédric Meuter	Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces.	FM	2006	DBLP DOI BibTeX RDF	testing of asynchronous distributed systems, global properties, model checking of traces, monitor
33	Wenhui Zhang	SAT-Based Verification of LTL Formulas.	FMICS/PDMC	2006	DBLP DOI BibTeX RDF
33	Barbara Jobstmann, Roderick Bloem	Optimizations for LTL Synthesis.	FMCAD	2006	DBLP DOI BibTeX RDF
33	Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi	Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking.	CAV	2005	DBLP DOI BibTeX RDF
33	Radek Pelánek, Jan Strejcek	Deeper Connections Between LTL and Alternating Automata.	CIAA	2005	DBLP DOI BibTeX RDF
33	Jiri Barnat, Lubos Brim, Ivana Cerná	Cluster-Based LTL Model Checking of Large Systems.	FMCO	2005	DBLP DOI BibTeX RDF
33	Timo Latvala, Marko Mäkelä	LTL Model Checking for Modular Petri Nets.	ICATPN	2004	DBLP DOI BibTeX RDF
33	Fang Wang, Sofiène Tahar, Otmane Aït Mohamed	First-Order LTL Model Checking Using MDGs.	ATVA	2004	DBLP DOI BibTeX RDF
33	Paul Gastin, Madhavan Mukund, K. Narayan Kumar	Local LTL with Past Constants Is Expressively Complete for Mazurkiewicz Traces.	MFCS	2003	DBLP DOI BibTeX RDF	concurrency, Temporal logics, Mazurkiewicz traces
33	Roberto Sebastiani, Stefano Tonetta	"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking.	CHARME	2003	DBLP DOI BibTeX RDF
33	Jiri Barnat, Lubos Brim, Jakub Chaloupka	Parallel Breadth-First Search LTL Model-Checking.	ASE	2003	DBLP DOI BibTeX RDF
33	Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani	Improving the Encoding of LTL Model Checking into SAT.	VMCAI	2002	DBLP DOI BibTeX RDF
33	Paul Gastin, Denis Oddoux	Fast LTL to Büchi Automata Translation.	CAV	2001	DBLP DOI BibTeX RDF
33	Michael Leuschel, Thierry Massart, Andrew Currie	How to Make FDR Spin LTL Model Checking of CSP by Refinement.	FME	2001	DBLP DOI BibTeX RDF
33	Javier Esparza, Keijo Heljanko	Implementing LTL Model Checking with Net Unfoldings.	SPIN	2001	DBLP DOI BibTeX RDF
33	Javier Esparza, Claus Schröter	Net Reductions for LTL Model-Checking.	CHARME	2001	DBLP DOI BibTeX RDF
33	Klaus Schneider 0001	Yet another Look at the LTL Model Checking.	CHARME	1999	DBLP DOI BibTeX RDF
33	Javier Esparza, Stephan Melzer	Model Checking LTL Using Constraint Programming.	ICATPN	1997	DBLP DOI BibTeX RDF
30	Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, Angelo Montanari	LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa.	TIME	2023	DBLP DOI BibTeX RDF
30	Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, Angelo Montanari	A Singly Exponential Transformation of LTL[X, F] into Pure Past LTL.	KR	2023	DBLP DOI BibTeX RDF
30	Jan Kretínský, Tobias Meggendorfer, Salomon Sickert	LTL Store: Repository of LTL formulae from literature and case studies.	CoRR	2018	DBLP BibTeX RDF
30	Ala-Eddine Ben Salem	Improving the model checking of stutter-invariant LTL properties. (Amélioration du model checking des propriétés LTL insensibles au bégaiement).		2014	RDF
30	Michaël Guedj	BSP Algorithms for LTL & CTL* Model Checking of Security Protocols. (Algorithmes BSP pour la vérification de modèles LTL et CTL* pour les protocoles de sécurité).		2012	RDF
30	Vineet Kahlon, Aarti Gupta	On the analysis of interacting pushdown systems.	POPL	2007	DBLP DOI BibTeX RDF	model checking, concurrency, dataflow analysis, LTL, mu-calculus, pushdown systems
30	Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat 0001	A Property-Driven Approach to Formal Verification of Process Models.	ICEIS (Selected Papers)	2007	DBLP DOI BibTeX RDF	Properties Validation, Temporal OCL, Models Semantics, Verification, Petri Nets, Process Model, Model Transformation, Metamodelling, LTL
30	Chao Wang 0001, Roderick Bloem, Gary D. Hachtel, Kavita Ravi, Fabio Somenzi	Compositional SCC Analysis for Language Emptiness.	Formal Methods Syst. Des.	2006	DBLP DOI BibTeX RDF	language emptiness, model checking, BDD, LTL, abstraction refinement
30	Xi Chen 0024, Harry Hsieh, Felice Balarin	Verification Approach of Metropolis Design Framework for Embedded Systems.	Int. J. Parallel Program.	2006	DBLP DOI BibTeX RDF	metropolis, simulation, formal verification, meta-model, spin, LTL, property, LOC
29	Malay K. Ganai, Aarti Gupta	Efficient BMC for Multi-Clock Systems with Clocked Specifications.	ASP-DAC	2007	DBLP DOI BibTeX RDF	OpenCores multiclock system benchmarks, clocked specifications, multiphased clocks, level-sensitive latches, SAT-based bounded model checking, synchronous multiclock systems, clocked LTL properties, clock modeling schemes, clock constraints, loop-checks, gated clocks
29	Kimmo Varpaaniemi	On Stubborn Sets in the Verification of Linear Time Temporal Properties.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	reduced state space generation, stubborn sets, verification of LTL formulas, reachability analysis
28	Astrid Rakow	Decompositional Petri Net Reductions.	IFM	2009	DBLP DOI BibTeX RDF
28	Thomas Noll 0001, Stefan Rieger	Verifying Dynamic Pointer-Manipulating Threads.	FM	2008	DBLP DOI BibTeX RDF
28	Amir Pnueli, Aleksandr Zaks	On the Merits of Temporal Testers.	25 Years of Model Checking	2008	DBLP DOI BibTeX RDF
28	Yogendra Narain Singh, Phalguni Gupta	Quantitative Evaluation of Normalization Techniques of Matching Scores in Multimodal Biometric Systems.	ICB	2007	DBLP DOI BibTeX RDF
28	Wenhui Zhang	Model Checking with SAT-Based Characterization of ACTL Formulas.	ICFEM	2007	DBLP DOI BibTeX RDF
28	Martin Leucker, César Sánchez 0001	Regular Linear Temporal Logic.	ICTAC	2007	DBLP DOI BibTeX RDF
28	Sven Schewe, Bernd Finkbeiner	Bounded Synthesis.	ATVA	2007	DBLP DOI BibTeX RDF
28	Michael Bauland, Thomas Schneider 0002, Henning Schnoor, Ilka Schnoor, Heribert Vollmer	The Complexity of Generalized Satisfiability for Linear Temporal Logic.	FoSSaCS	2007	DBLP DOI BibTeX RDF	computational complexity, linear temporal logic
28	Andreas Bauer 0002, Martin Leucker, Christian Schallhart	The Good, the Bad, and the Ugly, But How Ugly Is Ugly?	RV	2007	DBLP DOI BibTeX RDF
28	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems.	CADE	2007	DBLP DOI BibTeX RDF
28	Conghua Zhou	A compositional symbolic verification framework for concurrent software.	Infoscale	2007	DBLP DOI BibTeX RDF	model checking, composition, abstract, SAT
28	Matteo Dell'Amico, Maura Cerioli	DO-Casl: An Observer-Based Casl Extension for Dynamic Specifications.	AMAST	2006	DBLP DOI BibTeX RDF
28	Orna Kupferman, Robby Lampert	On the Construction of Fine Automata for Safety Properties.	ATVA	2006	DBLP DOI BibTeX RDF
28	Alessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta	From PSL to NBA: a Modular Symbolic Encoding.	FMCAD	2006	DBLP DOI BibTeX RDF
28	Christian Dax, Martin Hofmann 0001, Martin Lange	A Proof System for the Linear Time µ-Calculus.	FSTTCS	2006	DBLP DOI BibTeX RDF
28	Syed Suhaib, Deepak Mathaikutty, Sandeep K. Shukla, David Berner	XFM: An incremental methodology for developing formal models.	ACM Trans. Design Autom. Electr. Syst.	2005	DBLP DOI BibTeX RDF	Extreme formal modeling, prescriptive formal models, property ordering, property refactoring, formal specification, formal verification, extreme programming, SPIN, SMV
28	Ansuman Banerjee, Pallab Dasgupta	The open family of temporal logics: Annotating temporal operators with input constraints.	ACM Trans. Design Autom. Electr. Syst.	2005	DBLP DOI BibTeX RDF
28	Wil M. P. van der Aalst, H. T. de Beer, Boudewijn F. van Dongen	Process Mining and Verification of Properties: An Approach Based on Temporal Logic.	OTM Conferences (1)	2005	DBLP DOI BibTeX RDF	data mining, Petri nets, temporal logic, workflow management, business process management, Process mining
28	Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi	Regular Vacuity.	CHARME	2005	DBLP DOI BibTeX RDF
28	Stéphane Demri, Régis Gascon	Verification of Qualitative Constraints.	CONCUR	2005	DBLP DOI BibTeX RDF
28	Rajeev Alur, Kousha Etessami, P. Madhusudan	A Temporal Logic of Nested Calls and Returns.	TACAS	2004	DBLP DOI BibTeX RDF
28	Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato	Hierarchical and Recursive State Machines with Context-Dependent Properties.	ICALP	2003	DBLP DOI BibTeX RDF	Model Checking, Temporal Logic, Automata
28	Timo Latvala	Efficient Model Checking of Safety Properties.	SPIN	2003	DBLP DOI BibTeX RDF
28	Koushik Sen, Grigore Rosu, Gul Agha	Generating Optimal Linear Temporal Logic Monitors by Coinduction.	ASIAN	2003	DBLP DOI BibTeX RDF
28	Bozena Wozna, Andrzej Zbrzezny	Checking ACTL* Properties of Discrete Timed Automata via Bounded Model Checking.	FORMATS	2003	DBLP DOI BibTeX RDF
28	Orna Kupferman, Nir Piterman, Moshe Y. Vardi	Model Checking Linear Properties of Prefix-Recognizable Systems.	CAV	2002	DBLP DOI BibTeX RDF
28	Klaus Havelund, Grigore Rosu	Synthesizing Monitors for Safety Properties.	TACAS	2002	DBLP DOI BibTeX RDF
28	Moshe Y. Vardi	Branching vs. Linear Time: Final Showdown.	TACAS	2001	DBLP DOI BibTeX RDF
28	Thomas A. Henzinger, Rupak Majumdar	Symbolic Model Checking for Rectangular Hybrid Systems.	TACAS	2000	DBLP DOI BibTeX RDF
28	Françoise Bellegarde, Jacques Julliand, Olga Kouchnarenko	Ready-Simulation Is Not Ready to Express a Modular Refinement Relation.	FASE	2000	DBLP DOI BibTeX RDF
28	Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar	Rectangular Hybrid Games.	CONCUR	1999	DBLP DOI BibTeX RDF
28	Orna Kupferman, Moshe Y. Vardi	Modular Model Checking.	COMPOS	1997	DBLP DOI BibTeX RDF
28	Ahmed Bouajjani, Peter Habermehl	Constrained Properties, Semilinear Systems, and Petri Nets.	CONCUR	1996	DBLP DOI BibTeX RDF
28	Bengt Jonsson 0001, Yih-Kuen Tsay	Assumption/Guarantee Specifications in Linear-Time Temporal Logic (Extended Abstract).	TAPSOFT	1995	DBLP DOI BibTeX RDF
24	Lars Kuhtz, Bernd Finkbeiner	LTL Path Checking Is Efficiently Parallelizable.	ICALP (2)	2009	DBLP DOI BibTeX RDF
24	Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi	Falsification of LTL Safety Properties in Hybrid Systems.	TACAS	2009	DBLP DOI BibTeX RDF
24	Matthias Schmalz, Daniele Varacca, Hagen Völzer	Counterexamples in Probabilistic LTL Model Checking for Markov Chains.	CONCUR	2009	DBLP DOI BibTeX RDF
24	Jiri Barnat, Lubos Brim, Petr Rockai	DiVinE Multi-Core - A Parallel LTL Model-Checker.	ATVA	2008	DBLP DOI BibTeX RDF
24	Guangquan Zhang 0002, Rong Mei	An Approach of Concurrent Object-Oriented Program Slicing Based on LTL Property.	CSSE (2)	2008	DBLP DOI BibTeX RDF
24	Gordon Fraser 0001, Paul Ammann	Reachability and Propagation for LTL Requirements Testing.	QSIC	2008	DBLP DOI BibTeX RDF	requirements testing, software testing, automated testing, test case generation, property testing
24	Salamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach	Verification of Automatically Generated Pattern-Based LTL Specifications.	HASE	2007	DBLP DOI BibTeX RDF
24	Alessandro Armando, Roberto Carbone, Luca Compagna	LTL Model Checking for Security Protocols.	CSF	2007	DBLP DOI BibTeX RDF
24	Kais Klai, Laure Petrucci, Michel A. Reniers	An Incremental and Modular Technique for Checking LTL\X Properties of Petri Nets.	FORTE	2007	DBLP DOI BibTeX RDF
24	Jocelyn Simmonds, Jessica Davies 0001, Arie Gurfinkel, Marsha Chechik	Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC.	FMCAD	2007	DBLP DOI BibTeX RDF
24	Muffy Calder, Alice Miller 0001	Feature interaction detection by pairwise analysis of LTL properties - A case study.	Formal Methods Syst. Des.	2006	DBLP DOI BibTeX RDF	Distributed systems, Model checking, Feature interaction, Communicating processes, Communications services
24	Jaco Geldenhuys, Henri Hansen	Larger Automata and Less Work for LTL Model Checking.	SPIN	2006	DBLP DOI BibTeX RDF
24	Stefan Edelkamp, Shahid Jabbar	Large-Scale Directed Model Checking LTL.	SPIN	2006	DBLP DOI BibTeX RDF
24	Marius Kloetzer, Calin Belta	A Fully Automated Framework for Control of Linear Systems from LTL Specifications.	HSCC	2006	DBLP DOI BibTeX RDF
24	Peter Niebert, Doron A. Peled	Efficient Model Checking for LTL with Partial Order Snapshots.	TACAS	2006	DBLP DOI BibTeX RDF
24	Werner Damm, Guilherme Pinto, Stefan Ratschan	Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems.	ATVA	2005	DBLP DOI BibTeX RDF
24	Aidan Harding, Mark Ryan 0001, Pierre-Yves Schobbens	A New Algorithm for Strategy Synthesis in LTL Games.	TACAS	2005	DBLP DOI BibTeX RDF
24	Claus Schröter, Victor Khomenko	Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings.	CAV	2004	DBLP DOI BibTeX RDF
24	YoungMin Kwon, Gul Agha	Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains.	ICFEM	2004	DBLP DOI BibTeX RDF
24	Anca Muscholl, Igor Walukiewicz	An NP-Complete Fragment of LTL.	Developments in Language Theory	2004	DBLP DOI BibTeX RDF
24	Jaco Geldenhuys, Antti Valmari	Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient.	TACAS	2004	DBLP DOI BibTeX RDF
24	Lubos Brim, Ivana Cerná, Pavel Moravec 0002, Jirí Simsa	Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking.	FMCAD	2004	DBLP DOI BibTeX RDF
24	Amir Pnueli, Tamarah Arons	TLPVS: A PVS-Based LTL Verification System.	Verification: Theory and Practice	2003	DBLP DOI BibTeX RDF
24	Paul Gastin, Denis Oddoux	LTL with Past and Two-Way Very-Weak Alternating Automata.	MFCS	2003	DBLP DOI BibTeX RDF
24	Daniel Große, Rolf Drechsler	Formal verification of LTL formulas for SystemC designs.	ISCAS (5)	2003	DBLP DOI BibTeX RDF
24	Aidan Harding, Mark Ryan 0001, Pierre-Yves Schobbens	Towards Symbolic Strategy Synthesis for \left\langle {\left\langle A \right\rangle } \right\rangle-LTL.	TIME	2003	DBLP DOI BibTeX RDF
24	Dimitra Giannakopoulou, Flavio Lerda	From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata.	FORTE	2002	DBLP DOI BibTeX RDF
24	Stéphane Demri, Deepak D'Souza	An Automata-Theoretic Approach to Constraint LTL.	FSTTCS	2002	DBLP DOI BibTeX RDF
24	Lubos Brim, Ivana Cerná, Martin Necesal	Randomization Helps in LTL Model Checking.	PAPM-PROBMIV	2001	DBLP DOI BibTeX RDF
24	Jiri Barnat, Lubos Brim, Jitka Stríbrná	Distributed LTL Model-Checking in SPIN.	SPIN	2001	DBLP DOI BibTeX RDF
24	Javier Esparza, Antonín Kucera 0001, Stefan Schwoon	Model-Checking LTL with Regular Valuations for Pushdown Systems.	TACS	2001	DBLP DOI BibTeX RDF