Search results for "Linear Temporal Logic (LTL)"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Sergey Babenyshev, Vladimir V. Rybakov	Linear Temporal Logic LTL: Basis for Admissible Rules.	J. Log. Comput.	2011	DBLP DOI BibTeX RDF
1	Sergey Babenyshev, Vladimir V. Rybakov	Unification in linear temporal logic LTL.	Ann. Pure Appl. Logic	2011	DBLP DOI BibTeX RDF
1	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
1	Clemens Ley, Michael Benedikt	How big must complete XML query languages be?	ICDT	2009	DBLP DOI BibTeX RDF
1	Erez Petrank, Madanlal Musuvathi, Bjarne Steensgaard	Progress guarantee for parallel programs via bounded lock-freedom.	PLDI	2009	DBLP DOI BibTeX RDF	bounded lock-freedom, lock-freedom, progress guarantees, model checking, parallel computation
1	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
1	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
1	Franz Baader, Andreas Bauer 0002, Marcel Lippmann	Runtime Verification Using a Temporal Description Logic.	FroCos	2009	DBLP DOI BibTeX RDF
1	Yang Liu 0003, Jun Sun 0001, Jin Song Dong	Scalable Multi-core Model Checking Fairness Enhanced Systems.	ICFEM	2009	DBLP DOI BibTeX RDF
1	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
1	Sergey Babenyshev, Vladimir V. Rybakov	Temporal Logic for Modeling Discovery and Logical Uncertainty.	KES	2009	DBLP DOI BibTeX RDF	decidability algorithms, Kripke/Hintikka models, temporal logic, uncertainty, chance discovery
1	Franz Baader, Andreas Bauer 0002, Alwen Tiu	Matching Trace Patterns with Regular Policies.	LATA	2009	DBLP DOI BibTeX RDF
1	Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi	Falsification of LTL Safety Properties in Hybrid Systems.	TACAS	2009	DBLP DOI BibTeX RDF
1	Gordon Fraser, Franz Wotawa	Complementary Criteria for Testing Temporal Logic Properties.	TAP	2009	DBLP DOI BibTeX RDF
1	Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek	On decidability of LTL model checking for process rewrite systems.	Acta Inf.	2009	DBLP DOI BibTeX RDF
1	Orna Kupferman, Nir Piterman, Moshe Y. Vardi	From liveness to promptness.	Formal Methods in System Design	2009	DBLP DOI BibTeX RDF	Verification, Temporal logic, Liveness
1	Liang Xu, Wei Chen 0018, Yanyan Xu, Wenhui Zhang	Improved Bounded Model Checking for the Universal Fragment of CTL.	J. Comput. Sci. Technol.	2009	DBLP DOI BibTeX RDF	model checking algorithm, ACTL, SAT, software verification, bounded model checking
1	Sergey Babenyshev, Vladimir V. Rybakov	Decidability of Hybrid Logic with Local Common Knowledge Based on Linear Temporal Logic LTL.	CiE	2008	DBLP DOI BibTeX RDF	multi-agent logics, relational Kripke-Hintikka models, decidability algorithms, satisfiability, linear temporal logic, hybrid logics
1	Jun Sun 0001, Yang Liu 0003, Jin Song Dong, Jing Sun 0002	Compositional encoding for bounded model checking.	Frontiers of Computer Science in China	2008	DBLP DOI BibTeX RDF	Communication Sequential Processes (CSP), Linear Temporal Logic (LTL), bounded model checking
1	Ram Krishnan, Jianwei Niu, Ravi S. Sandhu, William H. Winsborough	Stale-safe security properties for group-based secure information sharing.	FMSE	2008	DBLP DOI BibTeX RDF	stale attributes, information sharing, security properties
1	Yang Liu 0003, Jun Sun 0001, Jin Song Dong	An analyzer for extended compositional process algebras.	ICSE Companion	2008	DBLP DOI BibTeX RDF	simulation, model checking, fairness, sat solvers
1	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
1	Marius Kloetzer, Cristian Mahulea, Calin Belta, Laura Recalde, Manuel Silva	Formal analysis of timed continuous Petri nets.	CDC	2008	DBLP DOI BibTeX RDF
1	Salamah Salamah, Ann Q. Gates	A Technique for Using Model Checkers to Teach Formal Specifications.	CSEE&T	2008	DBLP DOI BibTeX RDF
1	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
1	Gordon Fraser, 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
1	Jinji Yang, Kaile Su, Qingliang Chen	Improving Encoding Efficiency for Bounded Model Checking.	TASE	2008	DBLP DOI BibTeX RDF	encoding, SAT, Bounded Model Checking
1	Alessandro Cimatti, Marco Roveri, Stefano Tonetta	Symbolic Compilation of PSL.	IEEE Trans. on CAD of Integrated Circuits and Systems	2008	DBLP DOI BibTeX RDF
1	Karsten Sohr, Michael Drouineaud, Gail-Joon Ahn, Martin Gogolla	Analyzing and Managing Role-Based Access Control Policies.	IEEE Trans. Knowl. Data Eng.	2008	DBLP DOI BibTeX RDF	Access controls, Protection mechanisms
1	Boyan Yordanov, Calin Belta	Parameter Synthesis for Piecewise Affine Systems from Temporal Logic Specifications.	HSCC	2008	DBLP DOI BibTeX RDF	Formal Verification, Piecewise Affine Systems
1	Vladimir V. Rybakov	Multi-agent Logics with Interacting Agents Based on Linear Temporal Logic: Deciding Algorithms.	ICAISC	2008	DBLP DOI BibTeX RDF	multi-agent logic, knowledge based reasoning, relational Kripke/Hintikka models, decidability algorithms, hybrid logics
1	Matthew Staats, Mats Per Erik Heimdahl	Partial Translation Verification for Untrusted Code-Generators.	ICFEM	2008	DBLP DOI BibTeX RDF
1	Felicidad Aguado, Pedro Cabalar, Gilberto Pérez, Concepción Vidal	Strongly Equivalent Temporal Logic Programs.	JELIA	2008	DBLP DOI BibTeX RDF
1	Klaus Havelund	Runtime Verification of C Programs.	TestCom/FATES	2008	DBLP DOI BibTeX RDF
1	Martin De Wulf, Laurent Doyen, Nicolas Maquet, Jean-François Raskin	Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking.	TACAS	2008	DBLP DOI BibTeX RDF
1	Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro	The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties.	ESEC/SIGSOFT FSE	2007	DBLP DOI BibTeX RDF	bi-infinite time, satisfiability checking, temporal logic, bounded model checking
1	Sylvain Hallé, Roger Villemaire, Omar Cherkaoui, Boubker Ghandour	Model Checking Data-Aware Workflow Properties with CTL-FO+.	EDOC	2007	DBLP DOI BibTeX RDF
1	Salamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach	Verification of Automatically Generated Pattern-Based LTL Specifications.	HASE	2007	DBLP DOI BibTeX RDF
1	Marius Kloetzer, Calin Belta	Managing non-determinism in symbolic robot motion planning and control.	ICRA	2007	DBLP DOI BibTeX RDF
1	Hadas Kress-Gazit, Georgios E. Fainekos, George J. Pappas	From structured english to robot motion.	IROS	2007	DBLP DOI BibTeX RDF
1	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
1	Katsunori Nakamura, Akira Fusaoka	Reasoning About Hybrid Systems Based on a Nonstandard Model.	Australian Conference on Artificial Intelligence	2007	DBLP DOI BibTeX RDF
1	Barbara Jobstmann, Stefan J. Galler, Martin Weiglhofer, Roderick Bloem	Anzu: A Tool for Property Synthesis.	CAV	2007	DBLP DOI BibTeX RDF
1	Orna Kupferman, Nir Piterman, Moshe Y. Vardi	From Liveness to Promptness.	CAV	2007	DBLP DOI BibTeX RDF
1	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
1	Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn L. Talcott	LTL Model Checking.	All About Maude	2007	DBLP DOI BibTeX RDF
1	Alessandro Cimatti, Marco Roveri, Stefano Tonetta	Syntactic Optimizations for PSL Verification.	TACAS	2007	DBLP DOI BibTeX RDF
1	Max Goldman, Shmuel Katz	MAVEN: Modular Aspect Verification.	TACAS	2007	DBLP DOI BibTeX RDF
1	Marta Cialdea Mayer, Carla Limongelli, Andrea Orlandini, Valentina Poggioni	Linear temporal logic as an executable semantics for planning languages.	Journal of Logic, Language and Information	2007	DBLP DOI BibTeX RDF	Applied temporal logic, Knowledge representation, Artificial intelligence planning
1	Hong Liu, David P. Gluch	Templates and automation for temporal query generation.	ACM Southeast Regional Conference	2006	DBLP DOI BibTeX RDF	architecture analysis & design language, model checking, computation tree logic
1	Elankayer Sithirasenan, Saad Zafar, Vallipuram Muthukkumarasamy	Formal Verification of the IEEE 802.11i WLAN Security Protocol.	ASWEC	2006	DBLP DOI BibTeX RDF
1	Alessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta	From PSL to NBA: a Modular Symbolic Encoding.	FMCAD	2006	DBLP DOI BibTeX RDF
1	Ajitha Rajan	Coverage Metrics to Measure Adequacy of Black-Box Test Suites.	ASE	2006	DBLP DOI BibTeX RDF
1	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
1	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
1	Thomas Tuerk, Klaus Schneider, Mike Gordon	Model Checking PSL Using HOL and SMV.	Haifa Verification Conference	2006	DBLP DOI BibTeX RDF
1	Eric Bodden, Volker Stolz	Tracechecks: Defining Semantic Interfaces with Temporal Logic.	Software Composition	2006	DBLP DOI BibTeX RDF
1	Katia Hristova, Yanhong A. Liu	Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems.	VMCAI	2006	DBLP DOI BibTeX RDF
1	Xi Chen, Harry Hsieh, Felice Balarin	Verification Approach of Metropolis Design Framework for Embedded Systems.	International Journal of Parallel Programming	2006	DBLP DOI BibTeX RDF	metropolis, simulation, formal verification, meta-model, spin, LTL, property, LOC
1	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
1	Marc Aiguier, Pascale Le Gall, Delphine Longuet, Assia Touil	A Temporal Logic for Input Output Symbolic Transition Systems.	APSEC	2005	DBLP DOI BibTeX RDF	input output symbolic transition systems, strong bisimulation, temporal logic, refinement, adequacy
1	Mihalis Yannakakis, Kousha Etessami	Checking LTL Properties of Recursive Markov Chains.	QEST	2005	DBLP DOI BibTeX RDF
1	Yulin Ding, Yan Zhang	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
1	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	2005	DBLP DOI BibTeX RDF	data mining, Petri nets, temporal logic, workflow management, business process management, Process mining
1	Salamah Salamah, Ann Q. Gates, Steve Roach, Oscar Mondragon	Verifying Pattern-Generated LTL Formulas: A Case Study.	SPIN	2005	DBLP DOI BibTeX RDF
1	Thomas Tuerk, Klaus Schneider	From PSL to LTL: A Formal Validation in HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Radek Pelánek, Jan Strejcek	Deeper Connections Between LTL and Alternating Automata.	CIAA	2005	DBLP DOI BibTeX RDF
1	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
1	Howard Barringer, Allen Goldberg, Klaus Havelund, Koushik Sen	Program Monitoring with LTL in EAGLE.	IPDPS	2004	DBLP DOI BibTeX RDF
1	Michael Drouineaud, Maksym Bortin, Paolo Torrini, Karsten Sohr	A First Step Towards Formal Verification of Security Policy Properties for RBAC.	QSIC	2004	DBLP DOI BibTeX RDF
1	John Derrick, Graeme Smith	Linear Temporal Logic and Z Refinement.	AMAST	2004	DBLP DOI BibTeX RDF
1	Tamarah Arons	Verification of an Advanced mips-Type Out-of-Order Execution Algorithm.	CAV	2004	DBLP DOI BibTeX RDF
1	Hyoung Seok Hong, Hasan Ural	Using Model Checking for Reducing the Cost of Test Generation.	FATES	2004	DBLP DOI BibTeX RDF
1	Rajeev Alur, Kousha Etessami, P. Madhusudan	A Temporal Logic of Nested Calls and Returns.	TACAS	2004	DBLP DOI BibTeX RDF
1	Zhiming Liu, Anders P. Ravn, Xiaoshan Li	Unifying proof methodologies of duration calculus and timed linear temporal logic.	Formal Asp. Comput.	2004	DBLP DOI BibTeX RDF	Design, Verification, Real-time, Specification, Refinement
1	Klaus Havelund, Grigore Rosu	Efficient monitoring of safety properties.	STTT	2004	DBLP DOI BibTeX RDF	Monitoring, Temporal logics, Safety
1	Daniel Große, Rolf Drechsler	Formal verification of LTL formulas for SystemC designs.	ISCAS	2003	DBLP DOI BibTeX RDF
1	Marco Pistore, Moshe Y. Vardi	The Planning Spectrum - One, Two, Three, Infinity.	LICS	2003	DBLP DOI BibTeX RDF
1	Koushik Sen, Grigore Rosu, Gul Agha	Generating Optimal Linear Temporal Logic Monitors by Coinduction.	ASIAN	2003	DBLP DOI BibTeX RDF
1	Rajeev Alur, Salvatore La Torre, P. Madhusudan	Modular Strategies for Infinite Games on Recursive Graphs.	CAV	2003	DBLP DOI BibTeX RDF
1	Paulo Tabuada, George J. Pappas	Model Checking LTL over Controllable Linear Systems Is Decidable.	HSCC	2003	DBLP DOI BibTeX RDF
1	Frank D. Valencia	Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL.	ICLP	2003	DBLP DOI BibTeX RDF
1	Kirsten Winter, Graeme Smith	Compositional Verification for Object-Z.	ZB	2003	DBLP DOI BibTeX RDF
1	Michael J. C. Gordon	Validating the PSL/Sugar Semantics Using Automated Reasoning.	Formal Asp. Comput.	2003	DBLP DOI BibTeX RDF	Accellera, Property language, Sugar, Model checking, Semantics, Formal verification, Theorem proving, Higher-order logic, PSL, HOL
1	Klaus Havelund, Grigore Rosu	Synthesizing Monitors for Safety Properties.	TACAS	2002	DBLP DOI BibTeX RDF
1	Heikki Tauriainen, Keijo Heljanko	Testing LTL formula translation into Büchi automata.	STTT	2002	DBLP DOI BibTeX RDF	Model checking, Verification, Software testing, Temporal logic
1	Rajeev Alur, Kousha Etessami, Salvatore La Torre, Doron Peled	Parametric temporal logic for "model measuring".	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	model checking, temporal logic, quantitative analysis
1	Dimitra Giannakopoulou, Klaus Havelund	Automata-Based Verification of Temporal Properties on Running Programs.	ASE	2001	DBLP DOI BibTeX RDF
1	Klaus Havelund, Grigore Rosu	Monitoring Programs Using Rewriting.	ASE	2001	DBLP DOI BibTeX RDF
1	Zohar Manna, Henny Sipma	Alternating the Temporal Picture for Safety.	ICALP	2000	DBLP DOI BibTeX RDF
1	Rajeev Alur, Kousha Etessami, Salvatore La Torre, Doron Peled	Parametric Temporal Logic for "Model Measuring".	ICALP	1999	DBLP DOI BibTeX RDF
1	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
1	Grégoire Sutre, Alain Finkel, Olivier Roux, Franck Cassez	Effective Recognizability and Model Checking of Reactive Fiffo Automata.	AMAST	1998	DBLP DOI BibTeX RDF
1	Serenella Cerrito, Marta Cialdea Mayer	Bounded Model Search in Linear Temporal Logic and Its Application to Planning.	TABLEAUX	1998	DBLP DOI BibTeX RDF
1	Amir Pnueli, Elad Shahar	A Platform for Combining Deductive with Algorithmic Verification.	CAV	1996	DBLP DOI BibTeX RDF
1	Doron Peled, Thomas Wilke, Pierre Wolper	An Algorithmic Approach for Checking Closure Properties of omega-Regular Languages.	CONCUR	1996	DBLP DOI BibTeX RDF
1	Mahesh Girkar, Robert Moll	New Results on the Analysis of Concurrent Systems with an Infinite Number of Processes.	CONCUR	1994	DBLP DOI BibTeX RDF