BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
LTL
Google LTL

Tag #ltl

109 papers:

FMFM-2019-Jantsch0B0 #ambiguity #automaton
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata (SJ, DM0, CB, JK0), pp. 262–279.
ICSE-2019-ZhangHMBLU #named #source code #using
AutoTap: synthesizing and repairing trigger-action programs using LTL properties (LZ, WH, JM, NB, SL, BU), pp. 281–291.
CAVCAV-2019-LiVR #satisfiability
Satisfiability Checking for Mission-Time LTL (JL, MYV, KYR), pp. 3–22.
VMCAIVMCAI-2019-DeckerP #model checking #quantifier #using
Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic (ND, AP), pp. 513–534.
FMFM-2018-MenghiGPT #multi #nondeterminism
Multi-robot LTL Planning Under Uncertainty (CM, SG0, PP, JT), pp. 399–417.
MoDELSMoDELS-2018-BesnardBJTD #embedded #execution #modelling #uml #verification
Unified LTL Verification and Embedded Execution of UML Models (VB, MB, FJ, CT, PD), pp. 112–122.
CAVCAV-2018-BartocciBNR #finite #monitoring #semantics #specification
A Counting Semantics for Monitoring LTL Specifications over Finite Traces (EB, RB, DN, FR), pp. 547–564.
CAVCAV-2018-KretinskyMSZ #automaton
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (JK, TM, SS, CZ), pp. 567–577.
VMCAIVMCAI-2017-AhmedBBDFHINPRS #model checking
Bringing LTL Model Checking to Biologists (ZA, DB, SB, ACED, JF, BAH, SI, JN, NP, MR, NS), pp. 1–13.
SEFMSEFM-2016-BezdekBBC #automaton #parametricity #synthesis
LTL Parameter Synthesis of Parametric Timed Automata (PB, NB, JB, IC), pp. 172–187.
SEFMSEFM-2016-DobrikovLP #model checking
LTL Model Checking under Fairness in ProB (ID, ML, DP), pp. 204–211.
LATALATA-2015-Salem #automaton #model checking #testing
Single-Pass Testing Automata for LTL Model Checking (AEBS), pp. 563–576.
FMFM-2015-DuLT #independence #monitoring #policy #runtime
Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL (XD, YL, AT), pp. 231–247.
ASEASE-2015-LemieuxB #behaviour #mining #specification #using
Investigating Program Behavior Using the Texada LTL Specifications Miner (CL, IB), pp. 870–875.
ASEASE-2015-LemieuxPB #mining #specification
General LTL Specification Mining (T) (CL, DP, IB), pp. 81–92.
ESEC-FSEESEC-FSE-2015-MaozR #specification #synthesis
GR(1) synthesis for LTL specification patterns (SM, JOR), pp. 96–106.
ICSEICSE-v1-2015-BaresiKR #performance #scalability #specification #verification
Efficient Scalable Verification of LTL Specifications (LB, MMPK, MR), pp. 711–721.
TACASTACAS-2015-CiniF #proving #runtime #verification
An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.
TACASTACAS-2015-KiniV #automaton #probability
Limit Deterministic and Probabilistic Automata for LTL ∖ GU (DK, MV), pp. 628–642.
TACASTACAS-2015-MolnarDVB #incremental #induction #model checking #proving
Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.
CAVCAV-2015-DietschHLP #approach #model checking #modulo theories
Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.
IFMIFM-2014-SchneiderTWW #refinement
Managing LTL Properties in Event-B Refinement (SAS, HT, HW, DMW), pp. 221–237.
FSEFSE-2014-LiYP0H #finite #infinity #named #satisfiability
Aalta: an LTL satisfiability checker over Infinite/Finite traces (JL, YY, GP, LZ, JH), pp. 731–734.
TACASTACAS-2014-AlmagorBK
Discounting in LTL (SA, UB, OK), pp. 424–439.
CAVCAV-2014-CimattiGMT #hybrid #verification
Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.
CAVCAV-2014-EsparzaK #approach #automaton #composition
From LTL to Deterministic Automata: A Safraless Compositional Approach (JE, JK), pp. 192–208.
IJCARIJCAR-2014-Gore #fixpoint #logic
And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (RG), pp. 26–45.
LICSLICS-CSL-2014-MareticDB
Anchored LTL separation (GPM, MTD, DAB), p. 9.
VMCAIVMCAI-2014-KiniV #automaton #probability #safety #specification
Probabilistic Automata for Safety LTL Specifications (DK, MV), pp. 118–136.
QAPLQAPL-2013-Schuppan #satisfiability
Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance (VS), pp. 49–65.
TACASTACAS-2013-BenediktLW #markov #model checking
LTL Model Checking of Interval Markov Chains (MB, RL, JW), pp. 32–46.
TACASTACAS-2013-BohyBFR #specification #synthesis
Synthesis from LTL Specifications with Mean-Payoff Objectives (AB, VB, EF, JFR), pp. 169–184.
TACASTACAS-2013-SongT #detection #model checking
LTL Model-Checking for Malware Detection (FS, TT), pp. 416–431.
CAVCAV-2013-ChatterjeeGK #automaton #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 #model checking
A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.
CIAACIAA-2012-Mandrali
Weighted LTL with Discounting (EM), pp. 353–360.
FMFM-2012-BauerF #distributed #monitoring
Decentralised LTL Monitoring (AKB, YF), pp. 85–100.
KRKR-2012-FelliGL #multi #protocol #specification
Synthesizing Agent Protocols From LTL Specifications Against Multiple Partially-Observable Environments (PF, GDG, AL).
SEKESEKE-2012-SalamahEO #automaton #consistency #using
Consistency Checks of System Properties Using LTL and Büchi Automata (SS, ME, OO), pp. 39–44.
QAPLQAPL-2012-CormieBowinsB #model checking #probability
Measuring Progress of Probabilistic LTL Model Checking (ECB, FvB), pp. 33–47.
TACASTACAS-2012-BabiakKRS #automaton #performance
LTL to Büchi Automata Translation: Fast and More Deterministic (TB, MK, VR, JS), pp. 95–109.
CAVCAV-2012-BohyBFJR #synthesis
Acacia+, a Tool for LTL Synthesis (AB, VB, EF, NJ, JFR), pp. 652–657.
CAVCAV-2012-Ehlers #synthesis
ACTL ∩ LTL Synthesis (RE), pp. 39–54.
CAVCAV-2012-KretinskyE #automaton
Deterministic Automata for the (F, G)-Fragment of LTL (JK, JE), pp. 7–22.
IJCARIJCAR-2012-DemriDS
Taming Past LTL and Flat Counter Systems (SD, AKD, AS), pp. 179–193.
IFMIFM-J-2009-BenesBBCSV11 #automaton #component #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 #multi #satisfiability
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking (KYR, MYV), pp. 417–431.
SEFMSEFM-2011-MorseCNF #bound #model checking
Context-Bounded Model Checking of LTL Properties for ANSI-C Software (JM, LCC, DN, BF), pp. 302–317.
CAVCAV-2011-BaeM #model checking #parametricity
State/Event-Based LTL Model Checking under Parametric Generalized Fairness (KB, JM), pp. 132–148.
SEFMSEFM-2010-BersaniCFPR #constraints #integer #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 #monitoring #runtime
Cooperative Runtime Monitoring of LTL Interface Contracts (SH), pp. 227–236.
FoSSaCSFoSSaCS-2010-DemriS #decidability #model checking
When Model-Checking Freeze LTL over Counter Machines Becomes Decidable (SD, AS), pp. 176–190.
FoSSaCSFoSSaCS-2010-ToL #algorithm #decidability #infinity #model checking
Algorithmic Metatheorems for Decidable LTL Model Checking over Infinite Systems (AWT, LL), pp. 221–236.
CAVCAV-2010-CohenNS10a #composition #named #verification
SPLIT: A Compositional LTL Verifier (AC, KSN, YS), pp. 558–561.
ICALPICALP-v2-2009-KuhtzF
LTL Path Checking Is Efficiently Parallelizable (LK, BF), pp. 235–246.
IFMIFM-2009-BenesBCSVZ #partial order #reduction
Partial Order Reduction for State/Event LTL (NB, LB, IC, JS, PV, BZ), pp. 307–321.
IFMIFM-2009-VargasGTG #model checking
Model Checking LTL Formulae in RAISE with FDR (APV, AGG, SLTT, CG), pp. 231–245.
ASEASE-2009-BarnatBS #clustering #model checking
Cluster-Based I/O-Efficient LTL Model Checking (JB, LB, PS), pp. 635–639.
TACASTACAS-2009-PlakuKV #hybrid #safety
Falsification of LTL Safety Properties in Hybrid Systems (EP, LEK, MYV), pp. 368–382.
CAVCAV-2009-FiliotJR #algorithm
An Antichain Algorithm for LTL Realizability (EF, NJ, JFR), pp. 263–277.
VMCAIVMCAI-2009-GodefroidP #model checking #revisited
LTL Generalized Model Checking Revisited (PG, NP), pp. 89–104.
SEFMSEFM-2008-EdelkampS #model checking
Flash-Efficient LTL Model Checking with Minimal Counterexamples (SE, DS), pp. 73–82.
KRKR-2008-BaaderGL #axiom #logic
LTL over Description Logic Axioms (FB, SG, CL), pp. 684–694.
SEKESEKE-2008-GarciaRS #automation #named #verification
PROTEF: Automatic Verification of Pattern-Based LTL Templates (LG, SR, SS), pp. 261–266.
FoSSaCSFoSSaCS-2008-Bojanczyk
The Common Fragment of ACTL and LTL (MB), pp. 172–185.
FoSSaCSFoSSaCS-2008-DemriLS #automaton #model checking
Model Checking Freeze LTL over One-Counter Automata (SD, RL, AS), pp. 490–504.
TACASTACAS-2008-BarnatBSW #model checking
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking (JB, LB, PS, MW), pp. 48–62.
TACASTACAS-2008-WulfDMR #algorithm #anti #model checking #named #satisfiability
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking (MDW, LD, NM, JFR), pp. 63–77.
CAVCAV-2008-EdelkampSS #model checking
Semi-external LTL Model Checking (SE, PS, PS), pp. 530–542.
VMCAIVMCAI-2008-MorgensternS #automaton
From LTL to Symbolically Represented Deterministic Automata (AM, KS), pp. 279–293.
VMCAIVMCAI-2008-SohailSR #algorithm #game studies #hybrid
A Hybrid Algorithm for LTL Games (SS, FS, KR), pp. 309–323.
AMOSTA-MOST-2007-FraserW #generative #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 #model checking
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (JANP, AV), pp. 346–361.
FMFM-2006-GenonMM #algorithm #distributed #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.
TACASTACAS-2006-NiebertP #model checking #partial order #performance
Efficient Model Checking for LTL with Partial Order Snapshots (PN, DP), pp. 272–286.
CAVCAV-2006-RosuB #linear #logic #monitoring #synthesis
Allen Linear (Interval) Temporal Logic — Translation to LTL and Monitor Synthesis (GR, SB), pp. 263–277.
LICSLICS-2006-DemriL #automaton #quantifier
LTL with the Freeze Quantifier and Register Automata (SD, RL), pp. 17–26.
LICSLICS-2006-KahlonG #approach #model checking #thread
An Automata-Theoretic Approach for Model Checking Threads for LTL Propert (VK, AG), pp. 101–110.
DLTDLT-J-2004-MuschollW05
An NP-complete fragment of LTL (AM, IW), pp. 743–753.
CIAACIAA-2005-PelanekS #automaton
Deeper Connections Between LTL and Alternating Automata (RP, JS), pp. 238–249.
TACASTACAS-2005-HammerKM #model checking #on the fly
Truly On-the-Fly LTL Model Checking (MH, AK, SM), pp. 191–205.
TACASTACAS-2005-HardingRS #algorithm #game studies #synthesis
A New Algorithm for Strategy Synthesis in LTL Games (AH, MR, PYS), pp. 477–492.
TACASTACAS-2005-SchuppanB #model checking
Shortest Counterexamples for Symbolic Model Checking of LTL with Past (VS, AB), pp. 493–509.
CAVCAV-2005-SebastianiTV #hybrid #model checking
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.
VMCAIVMCAI-2005-LatvalaBHJ #bound #model checking #performance
Simple Is Better: Efficient Bounded Model Checking for Past LTL (TL, AB, KH, TAJ), pp. 380–395.
DLTDLT-2004-MuschollW
An NP-Complete Fragment of LTL (AM, IW), pp. 334–344.
ICALPICALP-2004-SamerV #query
A Syntactic Characterization of Distributive LTL Queries (MS, HV), pp. 1099–1110.
FoSSaCSFoSSaCS-2004-Demri #constraints #integer
LTL over Integer Periodicity Constraints: (SD), pp. 121–135.
TACASTACAS-2004-GeldenhuysV #algorithm #on the fly #performance #verification
Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient (JG, AV), pp. 205–219.
CAVCAV-2004-AbdullaJNdS #model checking
Regular Model Checking for LTL(MSO) (PAA, BJ, MN, Jd, MS), pp. 348–360.
CSLCSL-2004-Maier #liveness #safety
Intuitionistic LTL and a New Characterization of Safety and Liveness (PM), pp. 295–309.
ASEASE-2003-BarnatBC #model checking #parallel
Parallel Breadth-First Search LTL Model-Checking (JB, LB, JC), pp. 106–115.
TACASTACAS-2003-BenedettiC #bound #model checking
Bounded Model Checking for Past LTL (MB, AC), pp. 18–33.
CSLCSL-2003-KahlerW #complexity #model checking
Program Complexity of Dynamic LTL Model Checking (DK, TW), pp. 271–284.
ICLPICLP-2003-Valencia03a #concurrent #constraints #decidability #programming
Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL (FDV), pp. 422–437.
KRKR-2002-CalvaneseGV #reasoning
Reasoning about Actions and Planning in LTL Action Theories (DC, GDG, MYV), pp. 593–602.
SASSAS-2002-GallardoMP #model checking #refinement
Refinement of LTL Formulas for Abstract Model Checking (MdMG, PM, EP), pp. 395–410.
WRLAWRLA-2002-EkerMS #maude #model checking
The Maude LTL Model Checker (SE, JM, AS), pp. 162–187.
CSLCSL-2002-KuceraS #logic
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
Optimal Complexity Bounds for Positive LTL Games (JM, TT), pp. 262–275.
VMCAIVMCAI-2002-CimattiPRS #encoding #model checking #satisfiability
Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
FMFME-2001-LeuschelMC #csp #how #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 #performance
Fast LTL to Büchi Automata Translation (PG, DO), pp. 53–65.
LICSLICS-2001-AlurT #game studies #generative
Deterministic Generators and Games for LTL Fragments (RA, SLT), pp. 291–300.
ICALPICALP-2000-DiekertG
LTL Is Expressively Complete for Mazurkiewicz Traces (VD, PG), pp. 211–222.
ICALPICALP-2000-EsparzaH #approach #model checking
A New Unfolding Approach to LTL Model Checking (JE, KH), pp. 475–486.
CAVCAV-2000-SomenziB #automaton #performance
Efficient Büchi Automata from LTL Formulae (FS, RB), pp. 248–263.
CAVCAV-1998-Wallner #model checking #using
Model Checking LTL Using Net Unforldings (FW), pp. 207–218.
CAVCAV-1994-ClarkeGH #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.