BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
check (44)
model (43)
automata (16)
effici (10)
algorithm (8)

Stem ltl$ (all stems)

102 papers:

TACASTACAS-2015-CiniF #ltl #proving #runtime #verification
An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.
TACASTACAS-2015-KiniV #automaton #ltl #probability
Limit Deterministic and Probabilistic Automata for LTL ∖ GU (DK, MV), pp. 628–642.
TACASTACAS-2015-MolnarDVB #incremental #induction #ltl #model checking #proving
Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.
LATALATA-2015-Salem #automaton #ltl #model checking #testing
Single-Pass Testing Automata for LTL Model Checking (AEBS), pp. 563–576.
FMFM-2015-DuLT #independence #ltl #monitoring #policy #runtime
Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL (XD, YL, AT), pp. 231–247.
ESEC-FSEESEC-FSE-2015-MaozR #ltl #specification #synthesis
GR(1) synthesis for LTL specification patterns (SM, JOR), pp. 96–106.
ICSEICSE-v1-2015-BaresiKR #ltl #performance #scalability #specification #verification
Efficient Scalable Verification of LTL Specifications (LB, MMPK, MR), pp. 711–721.
CAVCAV-2015-DietschHLP #approach #ltl #model checking #modulo theories
Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.
CAVCAV-2015-FinkbeinerRS #algorithm #model checking
Algorithms for Model Checking HyperLTL and HyperCTL ^* (BF, MNR, CS), pp. 30–48.
FoSSaCSFoSSaCS-2014-AlmagorK #synthesis
Latticed-LTL Synthesis in the Presence of Noisy Inputs (SA, OK), pp. 226–241.
TACASTACAS-2014-AlmagorBK #ltl
Discounting in LTL (SA, UB, OK), pp. 424–439.
IFMIFM-2014-SchneiderTWW #ltl #refinement
Managing LTL Properties in Event-B Refinement (SAS, HT, HW, DMW), pp. 221–237.
FSEFSE-2014-LiYP0H #finite #infinity #ltl #named #satisfiability
Aalta: an LTL satisfiability checker over Infinite/Finite traces (JL, YY, GP, LZ, JH), pp. 731–734.
CAVCAV-2014-ChengHRS #automation #generative #named #source code
G4LTL-ST: Automatic Generation of PLC Programs (CHC, CHH, HR, SS), pp. 541–549.
CAVCAV-2014-CimattiGMT #hybrid #ltl #verification
Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.
CAVCAV-2014-EsparzaK #approach #automaton #composition #ltl
From LTL to Deterministic Automata: A Safraless Compositional Approach (JE, JK), pp. 192–208.
IJCARIJCAR-2014-Gore #fixpoint #logic #ltl
And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (RG), pp. 26–45.
LICSLICS-CSL-2014-MareticDB #ltl
Anchored LTL separation (GPM, MTD, DAB), p. 9.
VMCAIVMCAI-2014-KiniV #automaton #ltl #probability #safety #specification
Probabilistic Automata for Safety LTL Specifications (DK, MV), pp. 118–136.
TACASTACAS-2013-BenediktLW #ltl #markov #model checking
LTL Model Checking of Interval Markov Chains (MB, RL, JW), pp. 32–46.
TACASTACAS-2013-BohyBFR #ltl #specification #synthesis
Synthesis from LTL Specifications with Mean-Payoff Objectives (AB, VB, EF, JFR), pp. 169–184.
TACASTACAS-2013-SongT #detection #ltl #model checking
LTL Model-Checking for Malware Detection (FS, TT), pp. 416–431.
QAPLQAPL-2013-Schuppan #ltl #satisfiability
Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance (VS), pp. 49–65.
CAVCAV-2013-ChatterjeeGK #automaton #ltl #model checking #probability #synthesis
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis (KC, AG, JK), pp. 559–575.
CAVCAV-2013-EsparzaLNNSS #execution #ltl #model checking
A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.
TACASTACAS-2012-BabiakKRS #automaton #ltl #performance
LTL to Büchi Automata Translation: Fast and More Deterministic (TB, MK, VR, JS), pp. 95–109.
CIAACIAA-2012-Mandrali #ltl
Weighted LTL with Discounting (EM), pp. 353–360.
FMFM-2012-BauerF #distributed #ltl #monitoring
Decentralised LTL Monitoring (AKB, YF), pp. 85–100.
KRKR-2012-FelliGL #ltl #multi #protocol #specification
Synthesizing Agent Protocols From LTL Specifications Against Multiple Partially-Observable Environments (PF, GDG, AL).
SEKESEKE-2012-SalamahEO #automaton #consistency #ltl #using
Consistency Checks of System Properties Using LTL and Büchi Automata (SS, ME, OO), pp. 39–44.
QAPLQAPL-2012-CormieBowinsB #ltl #model checking #probability
Measuring Progress of Probabilistic LTL Model Checking (ECB, FvB), pp. 33–47.
CAVCAV-2012-BohyBFJR #ltl #synthesis
Acacia+, a Tool for LTL Synthesis (AB, VB, EF, NJ, JFR), pp. 652–657.
CAVCAV-2012-Ehlers #ltl #synthesis
ACTL ∩ LTL Synthesis (RE), pp. 39–54.
CAVCAV-2012-KretinskyE #automaton #ltl
Deterministic Automata for the (F, G)-Fragment of LTL (JK, JE), pp. 7–22.
IJCARIJCAR-2012-DemriDS #ltl
Taming Past LTL and Flat Counter Systems (SD, AKD, AS), pp. 179–193.
IFMIFM-J-2009-BenesBBCSV11 #automaton #component #ltl #partial order #reduction
Partial order reduction for state/event LTL with application to component-interaction automata (NB, LB, BB, IC, JS, PV), pp. 877–890.
FMFM-2011-RozierV #approach #encoding #ltl #multi #satisfiability
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking (KYR, MYV), pp. 417–431.
SEFMSEFM-2011-MorseCNF #bound #ltl #model checking
Context-Bounded Model Checking of LTL Properties for ANSI-C Software (JM, LCC, DN, BF), pp. 302–317.
CAVCAV-2011-BaeM #ltl #model checking #parametricity
State/Event-Based LTL Model Checking under Parametric Generalized Fairness (KB, JM), pp. 132–148.
FoSSaCSFoSSaCS-2010-DemriS #decidability #ltl #model checking
When Model-Checking Freeze LTL over Counter Machines Becomes Decidable (SD, AS), pp. 176–190.
FoSSaCSFoSSaCS-2010-ToL #algorithm #decidability #infinity #ltl #model checking
Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems (AWT, LL), pp. 221–236.
SEFMSEFM-2010-BersaniCFPR #constraints #integer #ltl #runtime #smt #specification #verification
SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability (MMB, LC, AF, MP, MR), pp. 244–254.
EDOCEDOC-2010-Halle #contract #interface #ltl #monitoring #runtime
Cooperative Runtime Monitoring of LTL Interface Contracts (SH), pp. 227–236.
CAVCAV-2010-CohenNS10a #composition #ltl #named #verification
SPLIT: A Compositional LTL Verifier (AC, KSN, YS), pp. 558–561.
ASEASE-2009-BarnatBS #clustering #ltl #model checking
Cluster-Based I/O-Efficient LTL Model Checking (JB, LB, PS), pp. 635–639.
TACASTACAS-2009-PlakuKV #hybrid #ltl #safety
Falsification of LTL Safety Properties in Hybrid Systems (EP, LEK, MYV), pp. 368–382.
ICALPICALP-v2-2009-KuhtzF #ltl
LTL Path Checking Is Efficiently Parallelizable (LK, BF), pp. 235–246.
IFMIFM-2009-BenesBCSVZ #ltl #partial order #reduction
Partial Order Reduction for State/Event LTL (NB, LB, IC, JS, PV, BZ), pp. 307–321.
IFMIFM-2009-VargasGTG #ltl #model checking
Model Checking LTL Formulae in RAISE with FDR (APV, AGG, SLTT, CG), pp. 231–245.
CAVCAV-2009-FiliotJR #algorithm #ltl
An Antichain Algorithm for LTL Realizability (EF, NJ, JFR), pp. 263–277.
VMCAIVMCAI-2009-GodefroidP #ltl #model checking #revisited
LTL Generalized Model Checking Revisited (PG, NP), pp. 89–104.
FoSSaCSFoSSaCS-2008-Bojanczyk #ltl
The Common Fragment of ACTL and LTL (MB), pp. 172–185.
FoSSaCSFoSSaCS-2008-DemriLS #automaton #ltl #model checking
Model Checking Freeze LTL over One-Counter Automata (SD, RL, AS), pp. 490–504.
TACASTACAS-2008-BarnatBSW #ltl #model checking
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking (JB, LB, PS, MW), pp. 48–62.
TACASTACAS-2008-WulfDMR #algorithm #anti #ltl #model checking #named #satisfiability
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking (MDW, LD, NM, JFR), pp. 63–77.
SEFMSEFM-2008-EdelkampS #ltl #model checking
Flash-Efficient LTL Model Checking with Minimal Counterexamples (SE, DS), pp. 73–82.
KRKR-2008-BaaderGL #axiom #logic #ltl
LTL over Description Logic Axioms (FB, SG, CL), pp. 684–694.
SEKESEKE-2008-GarciaRS #automation #ltl #named #verification
PROTEF: Automatic Verification of Pattern-Based LTL Templates (LG, SR, SS), pp. 261–266.
CAVCAV-2008-EdelkampSS #ltl #model checking
Semi-external LTL Model Checking (SE, PS, PS), pp. 530–542.
VMCAIVMCAI-2008-MorgensternS #automaton #ltl
From LTL to Symbolically Represented Deterministic Automata (AM, KS), pp. 279–293.
VMCAIVMCAI-2008-SohailSR #algorithm #game studies #hybrid #ltl
A Hybrid Algorithm for LTL Games (SS, FS, KR), pp. 309–323.
ICALPICALP-2007-TorreP #complexity #model checking #on the #recursion #state machine
On the Complexity of LtlModel-Checking of Recursive State Machines (SLT, GP), pp. 937–948.
AMOSTAMOST-2007-FraserW #generative #ltl #model checking #performance #testing #using
Using LTL rewriting to improve the performance of model-checker based test-case generation (GF, FW), pp. 64–74.
CADECADE-2007-PerezV #bound #effectiveness #encoding #logic #ltl #model checking
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (JANP, AV), pp. 346–361.
TACASTACAS-2006-NiebertP #ltl #model checking #partial order #performance
Efficient Model Checking for LTL with Partial Order Snapshots (PN, DP), pp. 272–286.
FMFM-2006-GenonMM #algorithm #distributed #ltl #monitoring #performance #sequence
Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces (AG, TM, CM), pp. 557–572.
CAVCAV-2006-RosuB #linear #logic #ltl #monitoring #synthesis
Allen Linear (Interval) Temporal Logic — Translation to LTL and Monitor Synthesis (GR, SB), pp. 263–277.
LICSLICS-2006-DemriL #automaton #ltl #quantifier
LTL with the Freeze Quantifier and Register Automata (SD, RL), pp. 17–26.
LICSLICS-2006-KahlonG #approach #ltl #model checking #thread
An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (VK, AG), pp. 101–110.
TACASTACAS-2005-HammerKM #ltl #model checking #on the fly
Truly On-the-Fly LTL Model Checking (MH, AK, SM), pp. 191–205.
TACASTACAS-2005-HardingRS #algorithm #game studies #ltl #synthesis
A New Algorithm for Strategy Synthesis in LTL Games (AH, MR, PYS), pp. 477–492.
TACASTACAS-2005-SchuppanB #ltl #model checking
Shortest Counterexamples for Symbolic Model Checking of LTL with Past (VS, AB), pp. 493–509.
DLTDLT-J-2004-MuschollW05 #ltl
An NP-complete fragment of LTL (AM, IW), pp. 743–753.
CIAACIAA-2005-PelanekS #automaton #ltl
Deeper Connections Between LTL and Alternating Automata (RP, JS), pp. 238–249.
CAVCAV-2005-SebastianiTV #hybrid #ltl #model checking
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.
ICLPICLP-2005-CorinSE #analysis #constraints #protocol #security
PS-LTL for Constraint-Based Security Protocol Analysis (RC, AS, SE), pp. 439–440.
VMCAIVMCAI-2005-LatvalaBHJ #bound #ltl #model checking #performance
Simple Is Better: Efficient Bounded Model Checking for Past LTL (TL, AB, KH, TAJ), pp. 380–395.
FoSSaCSFoSSaCS-2004-Demri #constraints #integer #ltl
LTL over Integer Periodicity Constraints: (Extended Abstract) (SD), pp. 121–135.
TACASTACAS-2004-GeldenhuysV #algorithm #ltl #on the fly #performance #verification
Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient (JG, AV), pp. 205–219.
DLTDLT-2004-MuschollW #ltl
An NP-Complete Fragment of LTL (AM, IW), pp. 334–344.
ICALPICALP-2004-SamerV #ltl #query
A Syntactic Characterization of Distributive LTL Queries (MS, HV), pp. 1099–1110.
CAVCAV-2004-AbdullaJNdS #ltl #model checking
Regular Model Checking for LTL(MSO) (PAA, BJ, MN, Jd, MS), pp. 348–360.
CAVCAV-2004-SchroterK #model checking #parallel #petri net
Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings (CS, VK), pp. 109–121.
CSLCSL-2004-Maier #liveness #ltl #safety
Intuitionistic LTL and a New Characterization of Safety and Liveness (PM), pp. 295–309.
ASEASE-2003-BarnatBC #ltl #model checking #parallel
Parallel Breadth-First Search LTL Model-Checking (JB, LB, JC), pp. 106–115.
TACASTACAS-2003-BenedettiC #bound #ltl #model checking
Bounded Model Checking for Past LTL (MB, AC), pp. 18–33.
CSLCSL-2003-KahlerW #complexity #ltl #model checking
Program Complexity of Dynamic LTL Model Checking (DK, TW), pp. 271–284.
ICLPICLP-2003-Valencia03a #concurrent #constraints #decidability #ltl #programming
Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL (FDV), pp. 422–437.
WRLAWRLA-2002-EkerMS #ltl #maude #model checking
The Maude LTL Model Checker (SE, JM, AS), pp. 162–187.
SASSAS-2002-GallardoMP #ltl #model checking #refinement
Refinement of LTL Formulas for Abstract Model Checking (MdMG, PM, EP), pp. 395–410.
KRKR-2002-CalvaneseGV #ltl #reasoning
Reasoning about Actions and Planning in LTL Action Theories (DC, GDG, MYV), pp. 593–602.
CSLCSL-2002-KuceraS #logic #ltl
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL (AK, JS), pp. 276–291.
CSLCSL-2002-MarcinkowskiT #bound #complexity #game studies #ltl
Optimal Complexity Bounds for Positive LTL Games (JM, TT), pp. 262–275.
VMCAIVMCAI-2002-CimattiPRS #encoding #ltl #model checking #satisfiability
Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
FMFME-2001-LeuschelMC #csp #how #ltl #model checking #refinement
How to Make FDR Spin LTL Model Checking of CSP by Refinement (ML, TM, AC), pp. 99–118.
CAVCAV-2001-GastinO #automaton #ltl #performance
Fast LTL to Büchi Automata Translation (PG, DO), pp. 53–65.
LICSLICS-2001-AlurT #game studies #generative #ltl
Deterministic Generators and Games for LTL Fragments (RA, SLT), pp. 291–300.
ICALPICALP-2000-DiekertG #ltl
LTL Is Expressively Complete for Mazurkiewicz Traces (VD, PG), pp. 211–222.
ICALPICALP-2000-EsparzaH #approach #ltl #model checking
A New Unfolding Approach to LTL Model Checking (JE, KH), pp. 475–486.
CAVCAV-2000-SomenziB #automaton #ltl #performance
Efficient Büchi Automata from LTL Formulae (FS, RB), pp. 248–263.
CAVCAV-1998-Wallner #ltl #model checking #using
Model Checking LTL Using Net Unforldings (FW), pp. 207–218.
CAVCAV-1994-ClarkeGH #ltl #model checking
Another Look at LTL Model Checking (EMC, OG, KH), pp. 415–427.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.