Search results for "TCTL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
106	Farn Wang, Geng-Dian Huang, Fang Yu 0001	TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering.	IEEE Trans. Software Eng.	2006	DBLP DOI BibTeX RDF	inevitability, non-Zeno, greatest fixpoint, real-time systems, model-checking, abstraction, TCTL
106	Farn Wang, Geng-Dian Hwang, Fang Yu 0001	TCTL Inevitability Analysis of Dense-Time Systems.	CIAA	2003	DBLP DOI BibTeX RDF	Branching temporal logics, inevitability, greatest fixpoint, real-time systems, model-checking, abstraction, TCTL
93	Jatindra Kumar Deka, Pallab Dasgupta, P. P. Chakrabarti 0001	An Efficiently Checkable Subset of TCTL for Formal Verification of Transition Systems with Delays.	VLSI Design	1999	DBLP DOI BibTeX RDF
79	Salvatore La Torre, Margherita Napoli	A Decidable Dense Branching-Time Temporal Logic.	FSTTCS	2000	DBLP DOI BibTeX RDF
76	Didier Lime, Olivier H. Roux, Charlotte Seidner, Louis-Marie Traonouez	Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches.	TACAS	2009	DBLP DOI BibTeX RDF	model-checking, tool, Time Petri nets, parameters, TCTL, stopwatches
64	Ana Fernández Vilas, José Juan Pazos-Arias, Ana Belén Barragáns-Martínez, Martín López Nores, Rebeca P. Díaz Redondo, Alberto Gil-Solla, Jorge García Duque, Manuel Ramos Cabrer	Multi-valued Model Checking in Dense-Time.	ECSQARU	2005	DBLP DOI BibTeX RDF	dense real-time, model checking, formal methods, multi-valued logic
64	François Laroussinie, Nicolas Markey, Philippe Schnoebelen	Model Checking Timed Automata with One or Two Clocks.	CONCUR	2004	DBLP DOI BibTeX RDF
60	Farn Wang	Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions.	ATVA	2008	DBLP DOI BibTeX RDF	time progress, model-checking, convex, Timed automaton, concave, TCTL
48	Jameleddine Hassine, Juergen Rilling, Rachida Dssouli	Use Case Maps as a property specification language.	Softw. Syst. Model.	2009	DBLP DOI BibTeX RDF	Temporal and architectural scope, Formal verification, Temporal logic, Use Case Maps, Property specification
48	Véronique Bruyère, Emmanuel Dall'Olio, Jean-François Raskin	Durations and parametric model-checking in timed automata.	ACM Trans. Comput. Log.	2008	DBLP DOI BibTeX RDF	model-checking, Timed automata, Presburger arithmetic
48	Houda Bel Mokadem, Béatrice Bérard, Patricia Bouyer, François Laroussinie	A New Modality for Almost Everywhere Properties in Timed Automata.	CONCUR	2005	DBLP DOI BibTeX RDF
48	Gerd Behrmann, Kim Guldstrand Larsen, Jacob Illum Rasmussen	Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness.	FORMATS	2005	DBLP DOI BibTeX RDF
48	Maria Sorea	Lazy Approximation for Dense Real-Time Systems.	FORMATS/FTRTFT	2004	DBLP DOI BibTeX RDF
48	Mustapha Bourahla, Mohamed Benmohamed	Verification of Real-Time Systems by Abstraction of Time Constraints.	IPDPS	2003	DBLP DOI BibTeX RDF	Real-time systems, Model Checking, Formal Verification, Predicate Abstraction, Timed Automaton
48	Véronique Bruyère, Emmanuel Dall'Olio, Jean-François Raskin	Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic.	STACS	2003	DBLP DOI BibTeX RDF
48	Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi	A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking.	CONCUR	1996	DBLP DOI BibTeX RDF
48	Satoshi Yamane	Verification system for real-time specification based on extended real-time logic.	RTCSA	1995	DBLP DOI BibTeX RDF	extended real-time logic, Timed CTL, verification system, bounded temporal operator, freeze quantification, real-time systems, formal specification, formal verification, temporal logic, real-time specification
46	Rachid Hadjidj, Hanifa Boucheneb	On-the-fly TCTL model checking for Time Petri Nets using state class graphs.	ACSD	2006	DBLP DOI BibTeX RDF
46	Wojciech Penczek, Bozena Wozna, Andrzej Zbrzezny	Towards Bounded Model Checking for the Universal Fragment of TCTL.	FTRTFT	2002	DBLP DOI BibTeX RDF
46	Martin Dickhöfer, Thomas Wilke	Timed Alternating Tree Automata: The Automata-Theoretic Solution to the TCTL Model Checking Problem.	ICALP	1999	DBLP DOI BibTeX RDF
44	Farn Wang	Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment.	HSCC	2009	DBLP DOI BibTeX RDF	algorithms, model-checking, experiment, timed automata, TCTL, branching bisimulation
32	Venkatesh Mysore, Carla Piazza, Bud Mishra	Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology.	ATVA	2005	DBLP DOI BibTeX RDF
32	Wojciech Penczek, Agata Pólrola	Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata.	ICATPN	2004	DBLP DOI BibTeX RDF
32	Farn Wang, Fang Yu 0001	OVL Assertion-Checking of Embedded Software with Dense-Time Semantics.	RTCSA	2003	DBLP DOI BibTeX RDF
32	Véronique Bruyère, Jean-François Raskin	Real-Time Model-Checking: Parameters Everywhere.	FSTTCS	2003	DBLP DOI BibTeX RDF
32	Marco Faella, Salvatore La Torre, Aniello Murano	Dense Real-Time Games.	LICS	2002	DBLP DOI BibTeX RDF
32	Udo Brockmeyer, Gunnar Wittich	Real-Time Verification of Statemate Designs.	CAV	1998	DBLP DOI BibTeX RDF
32	Farn Wang, Aloysius K. Mok, E. Allen Emerson	Symbolic Model Checking for Distributed Real-Time Systems.	FME	1993	DBLP DOI BibTeX RDF
32	Nathalie Rico, Gregor von Bochmann, Omar Cherkaoui	Model-Checking for Real-Time Systems Specified in Lotos.	CAV	1992	DBLP DOI BibTeX RDF
30	Leifeng He, Guanjun Liu	Prioritized Time-Point-Interval Petri Nets Modeling Multiprocessor Real-Time Systems and TCTL$_{x}$.	IEEE Trans. Ind. Informatics	2023	DBLP DOI BibTeX RDF
30	Chams Eddine Choucha, Mohamed Ramdani, Mohamed Khalgui, Laïd Kahloul	On Improvement of Formal Verification of Reconfigurable Real-Time Systems Using TCTL and CTL-Based Properties on IaaS Cloud Environment.	ICSOFT (Selected Papers)	2020	DBLP DOI BibTeX RDF
30	Ehsan Khamespanah, Ramtin Khosravi, Marjan Sirjani	An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models.	Sci. Comput. Program.	2018	DBLP DOI BibTeX RDF
30	Naima Jbeli, Zohra Sbaï, Rahma Ben Ayed	On the Fly Model-Checking of TPN: $$TPN-TCTL^{\varDelta }_{h}$$.	WorldCIST (2)	2018	DBLP DOI BibTeX RDF
30	Étienne André, Didier Lime, Mathias Ramparison	TCTL Model Checking Lower/Upper-Bound Parametric Timed Automata Without Invariants.	FORMATS	2018	DBLP DOI BibTeX RDF
30	Mohammad Esmail Esmaili, Reza Entezari-Maleki, Ali Movaghar 0001	Improved Region-Based TCTL Model Checking of Time Petri Nets.	J. Comput. Sci. Eng.	2015	DBLP DOI BibTeX RDF
30	Georges Morbé, Christoph Scholl 0001	Fully symbolic TCTL model checking for complete and incomplete real-time systems.	Sci. Comput. Program.	2015	DBLP DOI BibTeX RDF
30	Joakim Byg, Morten Jacobsen, Lasse Jacobsen, Kenneth Yrke Jørgensen, Mikael Harkjær Møller, Jirí Srba	TCTL-preserving translations from timed-arc Petri nets to networks of timed automata.	Theor. Comput. Sci.	2014	DBLP DOI BibTeX RDF
30	Ehsan Khamespanah, Ramtin Khosravi, Marjan Sirjani	Efficient TCTL Model Checking Algorithm for Timed Actors.	AGERE!@SPLASH	2014	DBLP DOI BibTeX RDF
30	Georges Morbé, Christoph Scholl 0001	Fully Symbolic TCTL Model Checking for Incomplete Timed Systems.	Electron. Commun. Eur. Assoc. Softw. Sci. Technol.	2013	DBLP DOI BibTeX RDF
30	Lasse Jacobsen, Morten Jacobsen, Mikael H. Møller, Jirí Srba	A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking.	EPEW	2010	DBLP DOI BibTeX RDF
30	Rachid Hadjidj, Hanifa Boucheneb	On-the-fly TCTL model checking for time Petri nets.	Theor. Comput. Sci.	2009	DBLP DOI BibTeX RDF
30	Hanifa Boucheneb, Guillaume Gardey, Olivier H. Roux	TCTL Model Checking of Time Petri Nets.	J. Log. Comput.	2009	DBLP DOI BibTeX RDF
30	Bozena Wozna, Andrzej Zbrzezny	Bounded Model Checking for the Existential Fragment of TCTL-G and Diagonal Timed Automata.	Fundam. Informaticae	2007	DBLP BibTeX RDF
30	Farn Wang, Geng-Dian Hwang, Fang Yu 0001	TCTL Inevitability Analysis of Dense-time Systems	CoRR	2003	DBLP BibTeX RDF
30	Anaheed Ayoub, Ayman M. Wahba, Ashraf M. Salem, Mohamed A. Sheirah	TCTL-Based Verification of Industrial Processes.	FDL	2003	DBLP BibTeX RDF
16	Dipankar Das 0002, P. P. Chakrabarti 0001, Rajeev Kumar 0004	Scenario-based timing verification of multiprocessor embedded applications.	ACM Trans. Design Autom. Electr. Syst.	2009	DBLP DOI BibTeX RDF	execution scenarios, real time systems, static timing analysis, Timing verification
16	Anna Dedova, Irina B. Virbitskaite	Towards Parametric Verification of Prioritized Time Petri Nets.	PaCT	2009	DBLP DOI BibTeX RDF
16	Morgan Magnin, Didier Lime, Olivier H. Roux	Symbolic State Space of Stopwatch Petri Nets with Discrete-Time Semantics (Theory Paper).	Petri Nets	2008	DBLP DOI BibTeX RDF	Verification using nets, symbolic state space, Time Petri nets, discrete-time, dense-time, stopwatches
16	Farn Wang, Geng-Dian Huang	Test Plan Generation for Concurrent Real-Time Systems Based on Zone Coverage Analysis.	TestCom/FATES	2008	DBLP DOI BibTeX RDF
16	Mohamed Khalgui, Hans-Michael Hanisch	NCES-based modelling and CTL-based verification of reconfigurable Benchmark Production Systems.	SIES	2008	DBLP DOI BibTeX RDF
16	Liang Xu	SMT-Based Bounded Model Checking for Real-Time Systems (Short Paper).	QSIC	2008	DBLP DOI BibTeX RDF	real-time systems, SMT, BMC
16	Louis-Marie Traonouez, Didier Lime, Olivier H. Roux	Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph.	FORMATS	2008	DBLP DOI BibTeX RDF	state-class graph, model-checking, Time Petri nets, parameters, stopwatches
16	David Walter, Scott Little, Nicholas Seegmiller, Chris J. Myers, Tomohiro Yoneda	Symbolic Model Checking of Analog/Mixed-Signal Circuits.	ASP-DAC	2007	DBLP DOI BibTeX RDF	analog/mixed-signal circuits, Boolean based symbolic model checking algorithm, VHDL-AMS description, labeled hybrid Petri nets, Boolean signals, temporal logic formulas, timed CTL, Boolean variables, Boolean function, binary decision diagram, hardware description language
16	Didier Lime, Olivier H. Roux	Model Checking of Time Petri Nets Using the State Class Timed Automaton.	Discret. Event Dyn. Syst.	2006	DBLP DOI BibTeX RDF	Dense-time systems, Model-checking, Timed automata, Time petri nets
16	Víctor A. Braberman, Alfredo Olivero, Fernando Schapachnik	Dealing with practical limitations of distributed timed model checking for timed automata.	Formal Methods Syst. Des.	2006	DBLP DOI BibTeX RDF	Distributed timed model checking, Kronos, Load-balance, Reconfiguration, Timed automata, Reachability, Redistribution, Zeus, DBM
16	Howard Bowman, Rodolfo Gómez 0001	How to stop time stopping.	Formal Aspects Comput.	2006	DBLP DOI BibTeX RDF	Zeno-timelocks, Non-zenoness conditions, Model checking, Timed automata
16	Farn Wang	REDLIB for the Formal Verification of Embedded Systems.	ISoLA	2006	DBLP DOI BibTeX RDF
16	Houda Bel Mokadem, Béatrice Bérard, Patricia Bouyer, François Laroussinie	Timed Temporal Logics for Abstracting Transient States.	ATVA	2006	DBLP DOI BibTeX RDF
16	Gabriel Leen, Donal Heffernan	Modeling and Verification of a Time-triggered Networking Protocol.	ICN/ICONS/MCL	2006	DBLP DOI BibTeX RDF
16	Víctor A. Braberman, Alfredo Olivero, Fernando Schapachnik	Issues in distributed timed model checking.	Int. J. Softw. Tools Technol. Transf.	2005	DBLP DOI BibTeX RDF	Distributed timed model checking, Kronos, Timed automata, Timed systems, Zeus
16	Nicolas Markey, Jean-François Raskin	Model Checking Restricted Sets of Timed Paths.	CONCUR	2004	DBLP DOI BibTeX RDF
16	Thomas Brihaye, Véronique Bruyère, Jean-François Raskin	Model-Checking for Weighted Timed Automata.	FORMATS/FTRTFT	2004	DBLP DOI BibTeX RDF
16	Libor Waszniowski, Zdenek Hanzálek	Analysis of Real Time Operating System Based Applications.	FORMATS	2003	DBLP DOI BibTeX RDF
16	Fernando Schapachnik, Víctor A. Braberman, Alfredo Olivero	An architecture-centric approach to the development of a distributed model-checker for timed automata.	ICSE	2002	DBLP DOI BibTeX RDF
16	Jatindra Kumar Deka, S. Chaki, Pallab Dasgupta, P. P. Chakrabarti 0001	Abstractions for model checking of event timings.	ISCAS (5)	2001	DBLP DOI BibTeX RDF
16	Luis Alejandro Cortés, Petru Eles, Zebo Peng	Verification of Embedded Systems using a Petri Net based Representation.	ISSS	2000	DBLP DOI BibTeX RDF
16	Hans Toetenel, Ronald F. Lutje Spelberg, G. Bandini	Parametric verification of the IEEE 1394a Root Contention protocol using LPMC.	RTCSA	2000	DBLP DOI BibTeX RDF	IEEE 1394a standard, Root Contention protocol, LPMC, PMC model checker, parameter relations, real-time model checking, parameter timing intervals, real-time systems, protocols, formal verification, randomization, telecommunication standards, linear constraints, IEEE standards, parametric verification
16	Irina B. Virbitskaite, E. Pokozy	A Partial Order Method for the Verification of Time Petri Nets.	FCT	1999	DBLP DOI BibTeX RDF
16	Irina B. Virbitskaite, E. Pokozy	Parametric Behaviour Analysis for Time Petri Nets.	PaCT	1999	DBLP DOI BibTeX RDF
16	Y. Tachi, Satoshi Yamane	Real-Time Symbolic Model Checking for Hard Real-Time Systems.	RTCSA	1999	DBLP DOI BibTeX RDF	real-time symbolic model checking, real-time systems, timed automaton, real-time temporal logic
16	Ahmed Bouajjani, Stavros Tripakis, Sergio Yovine	On-the-fly symbolic model checking for real-time systems.	RTSS	1997	DBLP DOI BibTeX RDF	on-the-fly symbolic model checking, timed temporal logic, boolean combinations, FDDI protocol verification, real-time systems, temporal logic, timed automaton, linear inequalities
16	Muriel Jourdan, Florence Maraninchi	Static Timing Analysis of Real-Time Systems.	Workshop on Languages, Compilers, & Tools for Real-Time Systems	1995	DBLP DOI BibTeX RDF
16	Liang Chen, Alistair Munro	Applications of Modal Logic for the Specification of Real-Time Systems.	FME	1993	DBLP DOI BibTeX RDF
16	Rajeev Alur, Costas Courcoubetis, David L. Dill	Model-Checking for Probabilistic Real-Time Systems (Extended Abstract).	ICALP	1991	DBLP DOI BibTeX RDF