Sign In

Ensuring Logic in the Fog: Sound POMDP Synthesis with LTL Objectives

μž‘μ„±μž
  • Haebom
μΉ΄ν…Œκ³ λ¦¬
Empty

μ €μž

Can Zhou, Yulong Gao, Pian Yu

πŸ’‘ κ°œμš”

λ³Έ 논문은 λΆˆν™•μ‹€ν•œ ν™˜κ²½μ—μ„œ λΆ€λΆ„μ μœΌλ‘œλ§Œ κ΄€μ°° κ°€λŠ₯ν•œ 마λ₯΄μ½”ν”„ κ²°μ • κ³Όμ •(POMDP) μƒμ—μ„œ μ„ ν˜• μ‹œκ°„ 논리(LTL)둜 λͺ…μ‹œλœ λ³΅μž‘ν•œ λͺ©ν‘œλ₯Ό λ§Œμ‘±ν•˜λŠ” 자율 μ—μ΄μ „νŠΈ 합성을 μœ„ν•œ μƒˆλ‘œμš΄ μ ‘κ·Ό 방식을 μ œμ•ˆν•œλ‹€. μ œμ•ˆλœ 방법은 LTL λ§Œμ‘±μ— κΈ°λ°˜ν•œ 동적인 μ‹ λ’°ν•  수 μžˆλŠ” 보상 ν•¨μˆ˜λ₯Ό μƒμ„±ν•˜κ³ , 이λ₯Ό λͺ¬ν…ŒμΉ΄λ₯Όλ‘œ κ³„νš ν”„λ ˆμž„μ›Œν¬μ— ν†΅ν•©ν•˜μ—¬ μ—μ΄μ „νŠΈκ°€ λΆ€λΆ„ κ΄€μ°° κ°€λŠ₯μ„±μ˜ λΆˆν™•μ‹€μ„± μ†μ—μ„œλ„ 검증 κ°€λŠ₯ν•œ 성곡을 μ΅œλŒ€ν™”ν•˜λ„λ‘ μœ λ„ν•œλ‹€. μ‹€ν—˜ κ²°κ³Ό, μ œμ•ˆλœ 방법이 κΈ°μ‘΄ 솔버가 μ‹€νŒ¨ν•˜λŠ” μ‹œλ‚˜λ¦¬μ˜€μ—μ„œλ„ μš°μˆ˜ν•˜λ©° λ‹€μ–‘ν•œ 벀치마크 λ„λ©”μΈμ—μ„œ νš¨κ³Όμ™€ ν™•μž₯성을 μœ μ§€ν•¨μ„ 보여쀀닀.

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

β€’
λΆ€λΆ„ κ΄€μ°° κ°€λŠ₯ ν™˜κ²½μ—μ„œ LTL λͺ©ν‘œ 달성을 μœ„ν•œ κ²¬κ³ ν•˜κ³  검증 κ°€λŠ₯ν•œ 보상 μ„€κ³„μ˜ μ€‘μš”μ„±μ„ κ°•μ‘°ν•œλ‹€.
β€’
λΆˆν™•μ‹€ν•œ ν™˜κ²½μ—μ„œ LTL μ œμ•½μ„ λ§Œμ‘±ν•˜λŠ” μ—μ΄μ „νŠΈ 합성을 μœ„ν•œ μ‹€μ§ˆμ μΈ ν”„λ ˆμž„μ›Œν¬λ₯Ό μ œκ³΅ν•œλ‹€.
β€’
μ œμ•ˆλœ λ°©λ²•μ˜ 이둠적 κΈ°λ°˜μ€ LTL 만쑱의 '인증'에 μžˆμ§€λ§Œ, μ‹€μ œ κ΅¬ν˜„μ—μ„œμ˜ 보상 ν•¨μˆ˜ 섀계 및 μ΅œμ ν™” λ‚œμ΄λ„λŠ” μ—¬μ „νžˆ μ‘΄μž¬ν•  수 μžˆλ‹€.
πŸ‘
Made with Slashpage