Sign In

LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning

Created by
  • Haebom
Category
Empty

μ €μž

Medina Andresel, Cristinel Mateis, Dejan Nickovic, Spyridon Kounoupidis, Panagiotis Katsaros, Stavros Tripakis

πŸ’‘ κ°œμš”

λ³Έ μ—°κ΅¬λŠ” λͺ¨ν˜Έν•˜κ³  λ‹€μ–‘ν•œ μžμ—°μ–΄ μš”κ΅¬μ‚¬ν•­μ„ μ„ ν˜• μ‹œκ°„ 논리(LTL) λͺ…μ„Έλ‘œ λ³€ν™˜ν•˜λŠ” 문제λ₯Ό ν•΄κ²°ν•˜κ³ μž ν•©λ‹ˆλ‹€. 특히, μž‘κ³  효율적인 μ–Έμ–΄ λͺ¨λΈ(40μ–΅-140μ–΅ νŒŒλΌλ―Έν„°)을 μ‚¬μš©ν•˜μ—¬ λ¬Έλ²•μ μœΌλ‘œ μœ νš¨ν•˜κ³  μΌκ΄€λœ LTL λͺ…μ„Έλ₯Ό μƒμ„±ν•˜λŠ” 데 쀑점을 λ‘‘λ‹ˆλ‹€. 이λ₯Ό μœ„ν•΄ LTLGuardλΌλŠ” λͺ¨λ“ˆμ‹ 도ꡬ체인을 κ°œλ°œν•˜μ—¬, μ œμ•½ μžˆλŠ” 생성과 κ²½λŸ‰μ˜ ν˜•μ‹μ  일관성 검사λ₯Ό κ²°ν•©ν•¨μœΌλ‘œμ¨ 좩돌 μ—†λŠ” LTL λͺ…μ„Έλ₯Ό μƒμ„±ν•©λ‹ˆλ‹€.

πŸ”‘ μ‹œμ‚¬μ  및 ν•œκ³„

β€’
μžμ› 효율적인 λͺ¨λΈμ„ ν™œμš©ν•œ LTL λͺ…μ„Έ 생성 κ°€λŠ₯μ„± μž…μ¦: μ†Œν˜• μ–Έμ–΄ λͺ¨λΈλ§ŒμœΌλ‘œλ„ LTL λͺ…μ„Έλ₯Ό 효과적으둜 생성할 수 μžˆμŒμ„ λ³΄μ—¬μ€λ‹ˆλ‹€.
β€’
λͺ¨λ“ˆμ‹ 도ꡬ체인을 ν†΅ν•œ λͺ…μ„Έ μƒμ„±μ˜ μ •ν™•μ„± 및 일관성 ν–₯상: 생성 λͺ¨λΈμ˜ μœ μ—°μ„±κ³Ό μžλ™ μΆ”λ‘ μ˜ 엄밀성을 κ²°ν•©ν•˜μ—¬ LTL λͺ…μ„Έμ˜ ν’ˆμ§ˆμ„ λ†’μ˜€μŠ΅λ‹ˆλ‹€.
β€’
μžμ—°μ–΄μ˜ λ³΅μž‘μ„± 및 κ²½λŸ‰ λͺ¨λΈμ˜ 본질적인 ν•œκ³„: μ—¬μ „νžˆ λ³΅μž‘ν•˜κ±°λ‚˜ λ―Έλ¬˜ν•œ μš”κ΅¬μ‚¬ν•­μ˜ 경우, κ²½λŸ‰ λͺ¨λΈμ΄ LTL의 λͺ¨λ“  츑면을 μ™„λ²½ν•˜κ²Œ μ΄ν•΄ν•˜κ³  λ³€ν™˜ν•˜λŠ” 데 어렀움을 κ²ͺ을 수 μžˆμŠ΅λ‹ˆλ‹€. λ˜ν•œ, LTLGuard 자체의 ν˜•μ‹μ  검증 λ²”μœ„μ™€ μΆ”λ‘  λŠ₯λ ₯의 ν•œκ³„λ„ μ‘΄μž¬ν•  수 μžˆμŠ΅λ‹ˆλ‹€.
πŸ‘
Made with Slashpage