Sign In

Automated Approach for Solving Infinite-state Polynomial Reachability Games

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

μ €μž

Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Maximilian Seeliger, {\DJ}or{\dj}e \v{Z}ikelic

πŸ’‘ κ°œμš”

λ³Έ 논문은 λ¬΄ν•œ μƒνƒœ 곡간을 κ°–λŠ” 닀항식 도달 κ°€λŠ₯μ„± κ²Œμž„μ—μ„œ REACH ν”Œλ ˆμ΄μ–΄κ°€ 승리 μ „λž΅μ„ κ°€μ§ˆ 수 μžˆλŠ”μ§€ κ²°μ •ν•˜κ³  κ³„μ‚°ν•˜λŠ” μžλ™ν™”λœ μ ‘κ·Ό 방식을 μ œμ•ˆν•©λ‹ˆλ‹€. REACH ν”Œλ ˆμ΄μ–΄μ˜ 승리λ₯Ό 증λͺ…ν•˜λŠ” μˆœμœ„ μΈμ¦μ„œ(ranking certificates)λΌλŠ” μƒˆλ‘œμš΄ 증λͺ… κ·œμΉ™μ„ λ„μž…ν–ˆμœΌλ©°, 이λ₯Ό 톡해 닀항식 μ œμ•½μœΌλ‘œ μ •μ˜λ˜λŠ” κ²Œμž„μ— λŒ€ν•œ μ™„μ „ μžλ™ν™”λœ 승리 μ „λž΅ 계산 μ•Œκ³ λ¦¬μ¦˜μ„ κ°œλ°œν–ˆμŠ΅λ‹ˆλ‹€. 이 μ•Œκ³ λ¦¬μ¦˜μ€ μ€€μ§€μˆ˜ μ‹œκ°„ λ³΅μž‘λ„λ‘œ μ‹€ν–‰λ˜λ©°, κΈ°μ‘΄ λ°©λ²•μœΌλ‘œλŠ” ν•΄κ²°ν•˜κΈ° μ–΄λ €μ› λ˜ λ³΅μž‘ν•œ μ˜ˆμ œμ—μ„œλ„ 효과적인 μ„±λŠ₯을 λ³΄μ—¬μ£Όμ—ˆμŠ΅λ‹ˆλ‹€.

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

β€’
닀항식 μ œμ•½μ„ κ°–λŠ” λ¬΄ν•œ μƒνƒœ 도달 κ°€λŠ₯μ„± κ²Œμž„μ— λŒ€ν•œ μ™„μ „ μžλ™ν™”λœ 승리 μ „λž΅ 계산 방법을 μ œμ‹œν•˜μ—¬, 인곡지λŠ₯ 및 λ°˜μ‘ ν•©μ„± λΆ„μ•Όμ˜ μ€‘μš”ν•œ 문제 해결에 κΈ°μ—¬ν•©λ‹ˆλ‹€.
β€’
μˆœμœ„ μΈμ¦μ„œλΌλŠ” 증λͺ… κ·œμΉ™μ€ REACH ν”Œλ ˆμ΄μ–΄μ˜ 승리 μ „λž΅ μ‘΄μž¬μ„±μ„ ν˜•μ‹μ μœΌλ‘œ 증λͺ…ν•˜λŠ” κ°•λ ₯ν•œ λ„κ΅¬λ‘œ ν™œμš©λ  수 μžˆμŠ΅λ‹ˆλ‹€.
β€’
μ œμ•ˆλœ μ•Œκ³ λ¦¬μ¦˜μ€ μ€€μ§€μˆ˜ μ‹œκ°„ λ³΅μž‘λ„λ₯Ό κ°€μ§€λ©°, κΈ°μ‘΄ λ°©λ²•μœΌλ‘œ ν•΄κ²° λΆˆκ°€λŠ₯ν–ˆλ˜ λ¬Έμ œμ— λŒ€ν•œ ν•΄κ²° κ°€λŠ₯성을 λ³΄μ—¬μ€λ‹ˆλ‹€.
β€’
λ³Έ μ—°κ΅¬λŠ” μ•Œκ³ λ¦¬μ¦˜μ˜ 완전성은 보μž₯ν•˜μ§€ μ•ŠμœΌλ©°(semi-complete), ν–₯ν›„ SAFE ν”Œλ ˆμ΄μ–΄μ˜ μ „λž΅ 계산 및 더 λ³΅μž‘ν•œ μ œμ•½ 쑰건을 λ‹€λ£¨λŠ” 연ꡬ가 ν•„μš”ν•©λ‹ˆλ‹€.
πŸ‘