본문 바로가기

전체 글

 (92)
Kripke 구조 예시 Kripke 구조 M = (S, S₀, R, AP, L)S = {s0, s1, s2}S₀ = {s0}R = {(s0, s1), (s1, s1), (s1, s2)}AP = {start, processing, done}L(s0) = {start}L(s1) = {processing}L(s2) = {done}이 구조는 다음과 같은 시스템을 나타냅니다:시작 상태는 s0이며, start 상태이다.s0에서 s1로 전이된다.s1은 processing 상태이고, 자기 자신으로 루프 가능.s1에서 s2로 갈 수 있으며, s2는 done 상태이다.---사용 예 (CTL 식 평가)EF done:s0에서 출발해 어떤 경로를 따라가면 언젠가 done 상태(s2)에 도달할 수 있다 → 참AG ¬done:모든 경로에서 d..
Kripke 구조 알겠습니다. 표 없이, 복사 가능한 텍스트 형식으로 정리해드리겠습니다:---Kripke 구조 (Kripke Structure)Kripke 구조 M은 다음과 같은 5개의 요소로 구성됩니다:M = (S, S₀, R, AP, L)S: 상태들의 집합 (State space)S₀: 초기 상태들의 집합, S₀ ⊆ SR: 상태 간 전이 관계, R ⊆ S × SAP: 원자 명제의 집합 (Atomic Propositions)L: 상태에 참인 원자 명제를 대응시키는 함수, L: S → 2^AP---예시S = {s₀, s₁, s₂}S₀ = {s₀}R = {(s₀, s₁), (s₁, s₂), (s₁, s₁)}AP = {start, ready, done}L(s₀) = {start}L(s₁) = {ready}L(s₂) = {do..
temporal logic **Temporal Logic(시계열 논리)**는 시간의 흐름에 따라 명제의 참/거짓을 표현할 수 있는 논리입니다. 즉, “지금 참”뿐 아니라 “항상 참”, “언젠가 참”, “곧 참일 것” 같은 시간적 개념을 기술할 수 있습니다.---왜 필요한가?전통적인 논리(명제논리, 술어논리)는 “언제” 참인지를 표현하지 못합니다.하지만 프로그램, 회로, 프로토콜처럼 시간에 따라 상태가 변하는 시스템에서는시간적 표현이 필수적입니다.---대표적인 Temporal Logic 종류

티스토리툴바