확률적 µ-계산의 산술적 만족 가능성 검사

본 논문은 모달 유사성 유형 Λ에 대한 coalgebraic µ-계산의 만족 가능성 검사 문제를 다룹니다. 이를 위해 기존의 tableau 규칙 기반 접근법을 일반화하여, 하나 단계 논리의 만족 가능성 문제의 복잡도에 의존하는 일반적인 지수 시간 상한을 제공합니다. 이를 통해 정수 가중치를 포함하는 등급 µ-계산 및 실수 가중치와 비선형 산술을 포함하는 확률적 µ-계산의 확장과 같이 기존 접근법으로는 다루기 어려운 사례들을 다룰 수 있습니다.