Search results for "CTL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
149	Laura Bozzelli	The Complexity of CTL* + Linear Past.	FoSSaCS	2008	DBLP DOI BibTeX RDF
112	Paritosh K. Pandya	Model Checking CTL*[DC].	TACAS	2001	DBLP DOI BibTeX RDF
110	Alexander Bolotov, Michael Fisher 0001	A Resolution Method For CTL Branching-Time Temporal Logic.	TIME	1997	DBLP DOI BibTeX RDF	resolution method, CTL branching-time temporal logic, clausal resolution method, extended CTL, fairness operators, step resolution, temporal resolution rule, linear-time temporal resolution, temporal logic, completeness, normal form, linear temporal logic, computation tree logic, CTL*
103	Orna Kupferman, Moshe Y. Vardi	An automata-theortetic approach to modular model checking.	ACM Trans. Program. Lang. Syst.	2000	DBLP DOI BibTeX RDF	temporal logic, automata, modular verification
102	Bernhard Josko	Modelchecking of CTL Formulae under Liveness Assumptions.	ICALP	1987	DBLP DOI BibTeX RDF
101	Ahmet Kara 0002, Volker Weber, Martin Lange, Thomas Schwentick	On the Hybrid Extension of CTL and CTL+.	MFCS	2009	DBLP DOI BibTeX RDF
94	Orna Kupferman, Moshe Y. Vardi	On the Complexity of Branching Modular Model Checking (Extended Abstract).	CONCUR	1995	DBLP DOI BibTeX RDF
93	Will Marrero	Using BDDs to Decide CTL.	TACAS	2005	DBLP DOI BibTeX RDF	validity, satisfiability, BDDs, CTL, tableau
92	Thomas Wilke	CTL+ is Exponentially more Succinct than CTL.	FSTTCS	1999	DBLP DOI BibTeX RDF
85	Moshe Y. Vardi	Branching vs. Linear Time: Final Showdown.	TACAS	2001	DBLP DOI BibTeX RDF
85	Orna Kupferman, Moshe Y. Vardi	Modular Model Checking.	COMPOS	1997	DBLP DOI BibTeX RDF
84	Zuan Zhang	An approach to hierarchy model checking via evaluating CTL hierarchically.	Asian Test Symposium	1995	DBLP DOI BibTeX RDF	hierarchy model checking, CTL specifications, computational complexity, formal specification, formal verification, Symbolic Model Checking, formal logic, CTL, logic partitioning, hierarchical systems, Computational Tree Logic, local properties
83	Thomas Ågotnes, Wiebe van der Hoek, Juan A. Rodríguez-Aguilar, Carles Sierra, Michael J. Wooldridge	Multi-Modal CTL: Completeness, Complexity, and an Application.	Stud Logica	2009	DBLP DOI BibTeX RDF	Computation Tree Logic (ctl), Social Laws, Normative Systems
76	Abhay Vardhan, Mahesh Viswanathan 0001	Learning to verify branching time properties.	Formal Methods Syst. Des.	2007	DBLP DOI BibTeX RDF	Verification, Learning, CTL
76	Marsha Chechik, Benet Devereux, Steve M. Easterbrook, Arie Gurfinkel	Multi-valued symbolic model-checking.	ACM Trans. Softw. Eng. Methodol.	2003	DBLP DOI BibTeX RDF	?Chek., model-checking, fairness, inconsistency, CTL, multi-valued logic, partiality
75	Jatindra Kumar Deka	Reasoning about Extremal Properties of Events.	TIME	2003	DBLP DOI BibTeX RDF
75	E. Allen Emerson, Joseph Y. Halpern	"Sometimes" and "Not Never" Revisited: On Branching Versus Linear Time.	POPL	1983	DBLP DOI BibTeX RDF
74	Wenhui Zhang	Bounded Semantics of CTL and SAT-Based Verification.	ICFEM	2009	DBLP DOI BibTeX RDF
74	Jiaqi Zhu, Hanpin Wang, Zhongyuan Xu	A New Temporal Logic CTL[k-QDDC] and Its Verification.	COMPSAC	2008	DBLP DOI BibTeX RDF	branching past, model checking, quantitative
74	Amir Pnueli, Yonit Kesten	A Deductive Proof System for CTL.	CONCUR	2002	DBLP DOI BibTeX RDF
73	Beata Konikowska, Wojciech Penczek	Reducing Model Checking from Multi-valued {\rm CTL}^{\ast} to {\rm CTL}^{\ast}.	CONCUR	2002	DBLP DOI BibTeX RDF
65	Tathagato Rai Dastidar, P. P. Chakrabarti 0001	A verification system for transient response of analog circuits.	ACM Trans. Design Autom. Electr. Syst.	2007	DBLP DOI BibTeX RDF	Ana CTL, model checking, query language, Analog circuits, equivalence checking, transient response
65	Dorel Lucanu, Gabriel Ciobanu	Model Checking for Object Specifications in Hidden Algebra.	VMCAI	2004	DBLP DOI BibTeX RDF	hidden algebra, object specification, behavioral bisimulation, CTL models, model checking, labeled transition systems, SMV
65	Hiroaki Iwashita, Tsuneo Nakata, Fumiyasu Hirose	CTL model checking based on forward state traversal.	ICCAD	1996	DBLP DOI BibTeX RDF	state traversal, partitioned transition relation, model checking, formal verification, CTL
65	Alessandro Ferrante, Margherita Napoli, Mimmo Parente	Graded-CTL: Satisfiability and Symbolic Model Checking.	ICFEM	2009	DBLP DOI BibTeX RDF
65	Lan Zhang 0001, Ullrich Hustadt, Clare Dixon	A Refined Resolution Calculus for CTL.	CADE	2009	DBLP DOI BibTeX RDF
65	Silvio do Lago Pereira, Leliane Nunes de Barros	Using alpha-ctl to Specify Complex Planning Goals.	WoLLIC	2008	DBLP DOI BibTeX RDF
65	Miaomiao Zhang, Dang Van Hung, Zhiming Liu 0001	Verification of Linear Duration Invariants by Model Checking CTL Properties.	ICTAC	2008	DBLP DOI BibTeX RDF
65	Wei Huang 0026, Zhonghua Wen, Yunfei Jiang, Aixiang Chen	Comparison Between Two Languages Used to Express Planning Goals: CTL and EAGLE.	PRICAI	2006	DBLP DOI BibTeX RDF
65	Thilo Hafer, Wolfgang Thomas	Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree.	ICALP	1987	DBLP DOI BibTeX RDF
64	Pieter Collins, Ivan S. Zapreev	Computable CTL* for Discrete-Time and Continuous-Space Dynamic Systems.	RP	2009	DBLP DOI BibTeX RDF	CTL *, Model Checking, Computability, Dynamic Systems
57	Abhay Vardhan, Mahesh Viswanathan 0001	Learning to verify branching time properties.	ASE	2005	DBLP DOI BibTeX RDF	CTL, computational learning theory, infinite state systems
56	Charles Pecheur, Franco Raimondi	Symbolic Model Checking of Logics with Actions.	MoChArt	2006	DBLP DOI BibTeX RDF
56	Tathagato Rai Dastidar, P. P. Chakrabarti 0001	A Verification System for Transient Response of Analog Circuits Using Model Checking.	VLSI Design	2005	DBLP DOI BibTeX RDF
56	Michael J. Wooldridge	Time, Knowledge, and Cooperation: Alternating-Time Temporal Epistemic Logic and Its Applications.	KI	2002	DBLP DOI BibTeX RDF
56	Michael J. Wooldridge, Wiebe van der Hoek	Time, Knowledge, and Cooperation: Alternating-Time Temporal Epistemic Logic and Its Applications.	COORDINATION	2002	DBLP DOI BibTeX RDF
56	Moshe Y. Vardi	Sometimes and Not Never Re-revisited: On Branching Versus Linear Time.	CONCUR	1998	DBLP DOI BibTeX RDF
56	Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton, Alberto L. Sangiovanni-Vincentelli	Equivalences for Fair Kripke Structures.	ICALP	1994	DBLP DOI BibTeX RDF
56	Batsayan Das, Dipankar Sarkar 0001, Santanu Chattopadhyay	Model checking on state transition diagram.	ASP-DAC	2004	DBLP DOI BibTeX RDF	CTL model checking, Finite State Machine (FSM), State Transition Diagram (STD), Kripke structure
56	Marcelo Finger, Renata Wassermann	Revising Specifications with CTL Properties Using Bounded Model Checking.	SBIA	2008	DBLP DOI BibTeX RDF	Model-checking, formal specification, belief revision, CTL
55	Sylvain Hallé, Roger Villemaire, Omar Cherkaoui, Boubker Ghandour	Model Checking Data-Aware Workflow Properties with CTL-FO+.	EDOC	2007	DBLP DOI BibTeX RDF
55	Ming-Hsien Tsai 0001, Bow-Yaw Wang	Formalization of CTL* in Calculus of Inductive Constructions.	ASIAN	2006	DBLP DOI BibTeX RDF
55	Yulin Ding, Yan Zhang 0003	Algorithms for CTL System Modification.	KES (2)	2005	DBLP DOI BibTeX RDF
55	Jan Johannsen, Martin Lange	CTL+ Is Complete for Double Exponential Time.	ICALP	2003	DBLP DOI BibTeX RDF
55	Cédric Roux, Emmanuelle Encrenaz	CTL May Be Ambiguous When Model Checking Moore Machines.	CHARME	2003	DBLP DOI BibTeX RDF
48	Graeme Smith 0001, Kirsten Winter	Model checking action system refinements.	Formal Aspects Comput.	2009	DBLP DOI BibTeX RDF	model checking, Refinement, CTL, action systems
48	Volker Weber	On the Complexity of Branching-Time Logics.	CSL	2009	DBLP DOI BibTeX RDF	complexity of satisfiability, pebble automata, alternating tree automata, forgettable past, CTL, branching-time logic
48	Alper Sen 0001, Vijay K. Garg	Detecting Temporal Logic Predicates on the Happened-Before Model.	IPDPS	2002	DBLP DOI BibTeX RDF	distributed systems, model checking, temporal logic, CTL, predicate detection
47	Sylvain Hallé, Roger Villemaire, Omar Cherkaoui, Jérôme Tremblay, Boubker Ghandour	Extending Model Checking to Data-Aware Temporal Properties of Web Services.	WS-FM	2007	DBLP DOI BibTeX RDF
47	Orna Kupferman, Moshe Y. Vardi	Memoryful Branching-Time Logic.	LICS	2006	DBLP DOI BibTeX RDF
47	Cécile Braunstein, Emmanuelle Encrenaz	Formalizing the Incremental Design and Verification Process of a Pipelined Protocol Converter.	IEEE International Workshop on Rapid System Prototyping	2006	DBLP DOI BibTeX RDF
47	Xiangyu Luo, Kaile Su, Abdul Sattar 0001, Mark Reynolds 0001	Verification of Multi-agent Systems Via Bounded Model Checking.	Australian Conference on Artificial Intelligence	2006	DBLP DOI BibTeX RDF	temporal epistemic logic, bounded semantics, multi-agent systems, bounded model checking
47	Thomas A. Henzinger, Rupak Majumdar, Vinayak S. Prabhu	Quantifying Similarities Between Timed Systems.	FORMATS	2005	DBLP DOI BibTeX RDF
47	Micah Adler, Neil Immerman	An n! lower bound on formula size.	ACM Trans. Comput. Log.	2003	DBLP DOI BibTeX RDF	lower bounds, temporal logic, Descriptive complexity
47	Alper Sen 0001, Vijay K. Garg	Detecting Temporal Logic Predicates in Distributed Programs Using Computation Slicing.	OPODIS	2003	DBLP DOI BibTeX RDF
47	David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen	Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae.	RTA	2002	DBLP DOI BibTeX RDF
47	Franz Weitl, Burkhard Freitag	Checking Content Consistency of Integrated Web Documents.	J. Comput. Sci. Technol.	2006	DBLP DOI BibTeX RDF	document verification, content consistency, temporal description logics, model checking, CTL -
46	Mark Reynolds 0001	A Tableau for CTL.	FM	2009	DBLP DOI BibTeX RDF
46	Junyan Qian, Lingzhong Zhao, Guoyong Cai, Tianlong Gu	Formula-Dependent Abstraction for CTL Model Checking.	ICCSA (2)	2008	DBLP DOI BibTeX RDF
46	Cécile Braunstein, Emmanuelle Encrenaz	CTL-property Transformations along an Incremental Design Process.	Int. J. Softw. Tools Technol. Transf.	2007	DBLP DOI BibTeX RDF	System design and verification, Computational tree logic, Simulation relation
46	Yulin Ding, Yan Zhang 0003	A Case Study for CTL Model Update.	KSEM	2006	DBLP DOI BibTeX RDF
46	Rachid Hadjidj, Hanifa Boucheneb	Much Compact Time Petri Net State Class Spaces Useful to Restore CTL* Properties.	ACSD	2005	DBLP DOI BibTeX RDF
46	Yulin Ding, Yan Zhang 0003	Model Updating CTL Systems.	Australian Conference on Artificial Intelligence	2005	DBLP DOI BibTeX RDF
46	Sharon Shoham, Orna Grumberg	Monotonic Abstraction-Refinement for CTL.	TACAS	2004	DBLP DOI BibTeX RDF
46	Sharon Shoham, Orna Grumberg	A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement.	CAV	2003	DBLP DOI BibTeX RDF
46	Sebastian Bauer 0004, Ian M. Hodkinson, Frank Wolter, Michael Zakharyaschev	On Non-Local Propositional and Local One-Variable Quantified CTL*.	TIME	2002	DBLP DOI BibTeX RDF
46	Abelardo Pardo, Gary D. Hachtel	Incremental CTL Model Checking Using BDD Subsetting.	DAC	1998	DBLP DOI BibTeX RDF	transceiver, spread spectrum communication, RF CMOS, digital radio, ISM frequency band
46	Adnan Aziz, Thomas R. Shiple, Vigyan Singhal	Formula-Dependent Equivalence for Compositional CTL Model Checking.	CAV	1994	DBLP DOI BibTeX RDF
46	Ramin Hojati, Robert K. Brayton, Robert P. Kurshan	BDD-Based Debugging Of Design Using Language Containment and Fair CTL.	CAV	1993	DBLP DOI BibTeX RDF
45	Rachid Hadjidj, Hanifa Boucheneb	Improving state class constructions for CTL* model checking of time Petri nets.	Int. J. Softw. Tools Technol. Transf.	2008	DBLP DOI BibTeX RDF	State class spaces, CTL* properties, Model checking, Formal methods, Time Petri nets
45	Zhi-Hong Tao, Conghua Zhou, Zhong Chen, Lifu Wang	Bounded Model Checking of CTL.	J. Comput. Sci. Technol.	2007	DBLP DOI BibTeX RDF	symbolic model checking, bounded model checking, QBF, CTL*
45	Jeffrey Ashley, Lawrence E. Holloway	An Equivalent CTL Formulation for Condition Sequences.	Discret. Event Dyn. Syst.	2005	DBLP DOI BibTeX RDF	computation tree logic (CTL), condition systems, temporal logic, discrete event systems (DES)
38	Astrid Rakow	Slicing Petri Nets with an Application to Workflow Verification.	SOFSEM	2008	DBLP DOI BibTeX RDF	Net Reduction, Workflow nets, Verification, Slicing, CTL
38	Graeme Smith 0001, John Derrick	Verifying data refinements using a model checker.	Formal Aspects Comput.	2006	DBLP DOI BibTeX RDF	State-based specifications, Z Refinement, Downward and upward simulations, Model checking, CTL
38	Benedikt Bollig, Paul Gastin	Weighted versus Probabilistic Logics.	Developments in Language Theory	2009	DBLP DOI BibTeX RDF
38	Benjamin Aminof, Axel Legay, Aniello Murano, Olivier Serre	µ-calculus Pushdown Module Checking with Imperfect State Information.	IFIP TCS	2008	DBLP DOI BibTeX RDF
38	Laura Bozzelli, Régis Gascon	Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints.	LPAR	2006	DBLP DOI BibTeX RDF
38	Bernhard Möller, Peter Höfner, Georg Struth	Quantales and Temporal Logics.	AMAST	2006	DBLP DOI BibTeX RDF
38	Laura Bozzelli	Complexity Results on Branching-Time Pushdown Model Checking.	VMCAI	2006	DBLP DOI BibTeX RDF
38	Bernd Finkbeiner, Sven Schewe	Semi-automatic Distributed Synthesis.	ATVA	2005	DBLP DOI BibTeX RDF
38	Xiangyu Luo, Kaile Su, Abdul Sattar 0001, Qingliang Chen, Guanfeng Lv	Bounded model checking knowledge and branching time in synchronous multi-agent systems.	AAMAS	2005	DBLP DOI BibTeX RDF	bounded semantics, temporal epistemic logic, translation to SAT, bounded model checking
38	Marko Samer, Helmut Veith	A Syntactic Characterization of Distributive LTL Queries.	ICALP	2004	DBLP DOI BibTeX RDF
38	Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga	Model Checking Discounted Temporal Properties.	TACAS	2004	DBLP DOI BibTeX RDF
38	Krishnendu Chatterjee, Pallab Dasgupta, P. P. Chakrabarti 0001	Complexity of Compositional Model Checking of Computation Tree Logic on Simple Structures.	IWDC	2004	DBLP DOI BibTeX RDF
38	Wiebe van der Hoek, Michael J. Wooldridge	Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications.	Stud Logica	2003	DBLP DOI BibTeX RDF	Cooperation logic, model checking, game theory, epistemic logic
38	Alexander Bolotov	A Clausal Resolution Method for Extended Computation Tree Logic ECTL.	TIME	2003	DBLP DOI BibTeX RDF
38	Ian M. Hodkinson, Frank Wolter, Michael Zakharyaschev	Decidable and Undecidable Fragments of First-Order Branching Temporal Logics.	LICS	2002	DBLP DOI BibTeX RDF
38	Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, Moshe Y. Vardi	Open Systems in Reactive Environments: Control and Synthesis.	CONCUR	2000	DBLP DOI BibTeX RDF
38	Orna Kupferman, Moshe Y. Vardi	Module Checking Revisited.	CAV	1997	DBLP DOI BibTeX RDF
38	Neil Immerman, Moshe Y. Vardi	Model Checking and Transitive-Closure Logic.	CAV	1997	DBLP DOI BibTeX RDF
38	Karlis Cerans	Deciding Properties of Integral Relational Automata.	ICALP	1994	DBLP DOI BibTeX RDF
38	Orna Bernholtz, Orna Grumberg	Branching Time Temporal Logic and Amorphous Tree Automata.	CONCUR	1993	DBLP DOI BibTeX RDF
38	Rocco De Nicola, Alessandro Fantechi, Stefania Gnesi, Gioia Ristori	An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems.	CAV	1991	DBLP DOI BibTeX RDF
38	Edmund M. Clarke, I. A. Draghicescu	Expressibility results for linear-time and branching-time logics.	REX Workshop	1988	DBLP DOI BibTeX RDF	linear-time logic, temporal logic, fairness, computation tree logics, branching-time logic
37	Sharon Shoham, Orna Grumberg	A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	3-valued semantics, Model checking games, Temporal logic, CTL, Counterexamples, Abstraction-Refinement
37	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
37	Tomás Brázdil, Vojtech Forejt, Jan Kretínský, Antonín Kucera 0001	The Satisfiability Problem for Probabilistic CTL.	LICS	2008	DBLP DOI BibTeX RDF	temporal logics, Markov chains
37	A. Prasad Sistla, Xiaodong Wang, Min Zhou	Checking extended CTL properties using guarded quotient structures.	Formal Methods Syst. Des.	2007	DBLP DOI BibTeX RDF	Symmetric systems, Guarded quotient structures, Model checking, Temporal logic, Program verification, State space reduction
37	Duminda Wijesekera, Paul Ammann, Lingya Sun, Gordon Fraser 0001	Relating counterexamples to test cases in CTL model checking specifications.	A-MOST	2007	DBLP DOI BibTeX RDF	test coverage criteria, model checking, formal methods, software testing, state machines, counterexamples
37	Loredana Afanasiev, Massimo Franceschet, Maarten Marx, Maarten de Rijke	CTL Model Checking for Processing Simple XPath Queries.	TIME	2004	DBLP DOI BibTeX RDF