Sign In

Incremental LTLf Synthesis

Created by
  • Haebom
Category
Empty

μ €μž

Giuseppe De Giacomo, Yves Lesperance, Gianmarco Parretti, Fabio Patrizi, Moshe Y. Vardi

πŸ’‘ κ°œμš”

λ³Έ 논문은 μ‹€ν–‰ 쀑에 λͺ©ν‘œκ°€ μ μ§„μ μœΌλ‘œ μ£Όμ–΄μ§€λŠ” λ°˜μ‘ν˜• ν•©μ„±μ˜ ν•œ ν˜•νƒœμΈ 점진적 LTLf 합성을 λ‹€λ£Ήλ‹ˆλ‹€. 이미 νŠΉμ • λͺ©ν‘œλ₯Ό μœ„ν•œ μ „λž΅μ„ μ‹€ν–‰ 쀑인 μ—μ΄μ „νŠΈκ°€ μƒˆλ‘œμš΄ λͺ©ν‘œλ₯Ό λ°›μœΌλ©΄, κΈ°μ‘΄ μ „λž΅μ„ ν¬κΈ°ν•˜κ³  초기 λͺ©ν‘œμ™€ μƒˆλ‘œμš΄ λͺ©ν‘œλ₯Ό λͺ¨λ‘ λ§Œμ‘±ν•˜λŠ” μƒˆλ‘œμš΄ μ „λž΅μ„ ν˜„μž¬ μ‹œμ λΆ€ν„° ν•©μ„±ν•΄μ•Ό ν•©λ‹ˆλ‹€. λ³Έ 논문은 점진적 ν•©μ„± 문제λ₯Ό ν˜•μ‹μ μœΌλ‘œ μ •μ˜ν•˜κ³  해결책을 μ œμ‹œν•©λ‹ˆλ‹€.

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

β€’
μžλ™ν™” 기반 ν•©μ„± 쀑에 κ΅¬μΆ•λœ 보쑰 데이터 ꡬ쑰λ₯Ό ν™œμš©ν•˜μ—¬ μ—¬λŸ¬ LTLf λͺ©ν‘œμ— λŒ€ν•œ 점진적 합성을 효율적으둜 μˆ˜ν–‰ν•˜λŠ” ν•΄κ²° 기법을 μ œμ•ˆν•©λ‹ˆλ‹€.
β€’
LTLf 곡식 진행에 κΈ°λ°˜ν•œ λŒ€μ•ˆμ μΈ ν•΄κ²° 기법을 κ³ λ €ν•˜λ©°, μ§„ν–‰λœ κ³΅μ‹μ˜ μ΅œμ†Œ μžλ™ν™” 크기가 원본 κ³΅μ‹μ˜ 크기λ₯Ό λ„˜μ§€ μ•ŠμŒμ„ λ³΄μ—¬μ€λ‹ˆλ‹€.
β€’
ν•˜μ§€λ§Œ, μƒˆλ‘œμš΄ λͺ©ν‘œκ°€ 도착할 λ•Œλ§ˆλ‹€ μ§„ν–‰λœ LTLf κ³΅μ‹μ˜ μžλ™ν™”λ₯Ό μ²˜μŒλΆ€ν„° λ‹€μ‹œ κ³„μ‚°ν•˜λŠ” λ‹¨μˆœ κ΅¬ν˜„μ€ 경쟁λ ₯이 μ—†μŒμ„ μ‹€ν—˜μ μœΌλ‘œ μž…μ¦ν•©λ‹ˆλ‹€.
πŸ‘