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