Chapter 1277. 유한 상태 머신 이론과 형식 모델 (FSM Theory and Formal Models)

• Chapter 1277. 유한 상태 머신 이론과 형식 모델 (FSM Theory and Formal Models)

• 1277.1유한 상태 머신의 역사적 배경

• 1277.2유한 상태 머신의 정의와 기본 개념

• 1277.3오토마타 이론과 유한 상태 머신의 관계

• 1277.4형식 언어와 유한 상태 머신

• 1277.5결정론적 유한 오토마타 (DFA)의 정의

• 1277.6결정론적 유한 오토마타의 형식적 표현

• 1277.7비결정론적 유한 오토마타 (NFA)의 정의

• 1277.8비결정론적 유한 오토마타의 형식적 표현

• 1277.9DFA와 NFA의 동치성 증명

• 1277.10NFA에서 DFA로의 부분 집합 구성법

• 1277.11ε-전이를 포함하는 NFA (ε-NFA)

• 1277.12ε-NFA에서 NFA로의 변환

• 1277.13상태 집합의 형식적 정의

• 1277.14입력 알파벳의 형식적 정의

• 1277.15전이 함수의 형식적 정의

• 1277.16초기 상태와 수용 상태의 형식적 정의

• 1277.17확장 전이 함수의 정의와 성질

• 1277.18상태 전이 다이어그램의 표현 방법

• 1277.19상태 전이 테이블의 표현 방법

• 1277.20정규 표현식과 유한 상태 머신의 관계

• 1277.21정규 표현식에서 NFA로의 변환 (Thompson 구성법)

• 1277.22NFA에서 정규 표현식으로의 변환 (상태 제거법)

• 1277.23정규 문법과 유한 상태 머신의 관계

• 1277.24우선형 문법과 유한 상태 머신

• 1277.25좌선형 문법과 유한 상태 머신

• 1277.26촘스키 계층 구조에서의 유한 상태 머신의 위치

• 1277.27유한 상태 머신의 최소화 이론

• 1277.28동치 상태의 정의와 판별

• 1277.29구별 불가능 상태와 Myhill-Nerode 정리

• 1277.30상태 최소화 알고리즘 (Hopcroft 알고리즘)

• 1277.31상태 최소화 알고리즘 (Moore 알고리즘)

• 1277.32최소 DFA의 유일성 정리

• 1277.33유한 상태 머신의 곱 구성

• 1277.34유한 상태 머신의 합집합 구성

• 1277.35유한 상태 머신의 교집합 구성

• 1277.36유한 상태 머신의 차집합 구성

• 1277.37유한 상태 머신의 여집합 구성

• 1277.38유한 상태 머신의 연결 (Concatenation) 구성

• 1277.39유한 상태 머신의 클리니 폐포 구성

• 1277.40유한 상태 머신의 동형 사상

• 1277.41Mealy 머신의 정의와 형식적 모델

• 1277.42Mealy 머신의 상태 전이와 출력 함수

• 1277.43Moore 머신의 정의와 형식적 모델

• 1277.44Moore 머신의 상태 전이와 출력 함수

• 1277.45Mealy 머신과 Moore 머신의 동치성

• 1277.46Mealy 머신에서 Moore 머신으로의 변환

• 1277.47Moore 머신에서 Mealy 머신으로의 변환

• 1277.48유한 상태 변환기 (Finite State Transducer)의 정의

• 1277.49변환기의 입력-출력 매핑

• 1277.50결정론적 변환기와 비결정론적 변환기

• 1277.51양방향 유한 오토마타 (2DFA)의 정의

• 1277.52양방향 유한 오토마타와 단방향 유한 오토마타의 동치성

• 1277.53확률적 유한 오토마타 (PFA)의 정의

• 1277.54확률적 전이 함수와 수용 확률

• 1277.55가중 유한 오토마타 (WFA)의 정의

• 1277.56가중 유한 오토마타의 반환 구조

• 1277.57양자 유한 오토마타 (QFA)의 개요

• 1277.58퍼지 유한 오토마타의 정의

• 1277.59퍼지 전이 함수와 멤버십 함수

• 1277.60시간 제약 유한 상태 머신 (Timed FSM)의 정의

• 1277.61시간 제약 유한 상태 머신의 클록과 가드 조건

• 1277.62통신 유한 상태 머신 (CFSM)의 정의

• 1277.63통신 유한 상태 머신의 채널 모델

• 1277.64입출력 유한 상태 머신 (IOFSM)의 정의

• 1277.65유한 상태 머신의 도달 가능성 분석

• 1277.66유한 상태 머신의 교착 상태 검출

• 1277.67유한 상태 머신의 생존성 분석

• 1277.68유한 상태 머신의 안전성 속성 검증

• 1277.69유한 상태 머신의 활동성 속성 검증

• 1277.70유한 상태 머신의 공정성 속성

• 1277.71모델 검사와 유한 상태 머신

• 1277.72시간 논리 (Temporal Logic)를 이용한 속성 명세

• 1277.73LTL (Linear Temporal Logic)과 유한 상태 머신

• 1277.74CTL (Computation Tree Logic)과 유한 상태 머신

• 1277.75CTL* 논리와 유한 상태 머신

• 1277.76Büchi 오토마타와 ω-정규 언어

• 1277.77Rabin 오토마타와 Streett 오토마타

• 1277.78Muller 오토마타의 정의

• 1277.79상태 폭발 문제의 정의와 원인

• 1277.80상태 폭발 완화를 위한 추상화 기법

• 1277.81기호적 모델 검사 (Symbolic Model Checking)

• 1277.82BDD (Binary Decision Diagram) 기반 상태 표현

• 1277.83SAT 기반 유계 모델 검사

• 1277.84반례 기반 추상화 정제 (CEGAR)

• 1277.85유한 상태 머신의 합성 방법론

• 1277.86사양으로부터의 자동 합성

• 1277.87반응형 합성 (Reactive Synthesis)의 개요

• 1277.88게임 이론적 접근을 통한 합성

• 1277.89유한 상태 머신의 대수적 표현

• 1277.90반군 (Semigroup)과 유한 상태 머신

• 1277.91모노이드 (Monoid)와 유한 상태 머신

• 1277.92구문 모노이드 (Syntactic Monoid)의 정의

• 1277.93Green 관계와 유한 상태 머신의 대수적 분류

• 1277.94Krohn-Rhodes 분해 정리

• 1277.95유한 상태 머신의 카테고리론적 해석

• 1277.96유한 상태 머신의 범주 (Category of FSM)

• 1277.97상태 머신의 함자 (Functor)와 자연 변환

• 1277.98코알지브라적 관점에서의 상태 머신

• 1277.99유한 상태 머신의 쌍대성 (Duality)

• 1277.100확장 유한 상태 머신 (EFSM)의 정의

• 1277.101확장 유한 상태 머신의 변수와 가드 조건

• 1277.102확장 유한 상태 머신의 실행 의미론

• 1277.103EFSM과 FSM의 관계 및 차이

• 1277.104주석 유한 상태 머신 (Annotated FSM)

• 1277.105계층적 상태 머신 (Hierarchical FSM)의 형식 모델

• 1277.106Harel Statecharts의 형식적 정의

• 1277.107Statecharts의 깊이 우선 상태 활성화

• 1277.108Statecharts의 직교 영역 (Orthogonal Regions)

• 1277.109Statecharts의 역사 상태 (History States)

• 1277.110Statecharts의 이벤트 방송 메커니즘

• 1277.111Statecharts의 실행 의미론 (Run-to-Completion)

• 1277.112UML 상태 머신 다이어그램의 형식 모델

• 1277.113UML 상태 머신의 단순 상태와 복합 상태

• 1277.114UML 상태 머신의 의사 상태 (Pseudostates)

• 1277.115UML 상태 머신의 진입/퇴장/행위 동작

• 1277.116UML 상태 머신의 지연 이벤트

• 1277.117UML 상태 머신의 프로토콜 상태 머신

• 1277.118SysML 상태 머신의 확장

• 1277.119페트리 넷과 유한 상태 머신의 비교

• 1277.120페트리 넷의 형식적 정의

• 1277.121페트리 넷의 도달 가능성과 커버 가능성

• 1277.122유한 상태 머신과 페트리 넷의 상호 변환

• 1277.123프로세스 대수와 유한 상태 머신

• 1277.124CCS (Calculus of Communicating Systems)와 FSM

• 1277.125CSP (Communicating Sequential Processes)와 FSM

• 1277.126π-계산법과 유한 상태 머신

• 1277.127유한 상태 머신에 의한 시퀀스 인식

• 1277.128유한 상태 머신에 의한 패턴 매칭

• 1277.129유한 상태 머신에 의한 프로토콜 명세

• 1277.130유한 상태 머신에 의한 프로토콜 검증

• 1277.131유한 상태 머신 기반 적합성 시험 (Conformance Testing)

• 1277.132전이 투어 (Transition Tour) 기법

• 1277.133구별 시퀀스 (Distinguishing Sequence) 기법

• 1277.134W-방법과 Wp-방법

• 1277.135UIO 시퀀스 기법

• 1277.136유한 상태 머신의 학습 이론 개요

• 1277.137Angluin의 L* 알고리즘

• 1277.138능동적 오토마타 학습 (Active Automata Learning)

• 1277.139수동적 오토마타 학습 (Passive Automata Learning)

• 1277.140RPNI (Regular Positive and Negative Inference) 알고리즘

• 1277.141유한 상태 머신 학습의 수렴 보장

• 1277.142반례 처리와 가설 정제

• 1277.143로봇공학에서 유한 상태 머신의 역할

• 1277.144로봇 행동 모델링을 위한 상태 정의

• 1277.145로봇 전이 조건의 이벤트 기반 설계

• 1277.146로봇 임무 수행을 위한 상태 순서 설계

• 1277.147로봇 상태 머신의 결정론적 요구 사항

• 1277.148로봇 상태 머신의 비결정론적 확장 가능성

• 1277.149로봇 행동 제어에서 Mealy 모델의 적용

• 1277.150로봇 행동 제어에서 Moore 모델의 적용

• 1277.151로봇 시스템에서의 확장 유한 상태 머신 적용

• 1277.152로봇 시스템에서의 계층적 상태 머신 적용

• 1277.153로봇 시스템에서의 상태 폭발 관리 전략

• 1277.154로봇 FSM 모델의 형식 검증 사례

• 1277.155자율 로봇 행동 제어를 위한 FSM 설계 패턴

• 1277.156드론 비행 모드 전환을 위한 FSM 모델링

• 1277.157드론 임무 단계 전이의 형식적 표현

• 1277.158다중 로봇 시스템에서의 FSM 조합 기법

• 1277.159ROS2 기반 상태 머신 구현에서의 형식 모델 활용

• 1277.160FSM 형식 모델의 시뮬레이션 검증 기법

• 1277.161FSM 형식 모델의 코드 자동 생성 기법

• 1277.162FSM 형식 모델 기반 테스트 케이스 자동 생성

• 1277.163유한 상태 머신의 형식적 등가 관계 (Bisimulation)

• 1277.164약한 이등가 (Weak Bisimulation)

• 1277.165분기 이등가 (Branching Bisimulation)

• 1277.166시뮬레이션 관계 (Simulation Relation)

• 1277.167트레이스 등가 (Trace Equivalence)

• 1277.168관찰 등가 (Observational Equivalence)

• 1277.169유한 상태 머신의 정제 (Refinement) 관계

• 1277.170유한 상태 머신의 추상화 (Abstraction) 기법

• 1277.171유한 상태 머신의 구성적 모델링 (Compositional Modeling)

• 1277.172동기적 합성 (Synchronous Composition)

• 1277.173비동기적 합성 (Asynchronous Composition)

• 1277.174인터리빙 합성 (Interleaving Composition)

• 1277.175유한 상태 머신의 계측 가능성과 관찰 가능성

• 1277.176부분 관찰 가능 유한 상태 머신

• 1277.177유한 상태 머신의 진단 가능성 (Diagnosability)

• 1277.178유한 상태 머신 기반 고장 진단 모델

• 1277.179유한 상태 머신의 불투명성 (Opacity) 분석

• 1277.180유한 상태 머신의 감독 제어 이론 (Supervisory Control Theory)

• 1277.181Ramadge-Wonham 프레임워크

• 1277.182제어 가능 이벤트와 관찰 가능 이벤트

• 1277.183최대 허용 감독자 (Supremal Controllable Supervisor)

• 1277.184모듈화된 감독 제어

• 1277.185분산 감독 제어

• 1277.186유한 상태 머신 형식 모델의 도구 지원 개요

• 1277.187UPPAAL을 이용한 시간 오토마타 모델링

• 1277.188SPIN 모델 검사기와 Promela 언어

• 1277.189NuSMV를 이용한 기호적 모델 검사

• 1277.190TLA+를 이용한 형식 명세

• 1277.191Alloy를 이용한 유한 상태 모델 분석

• 1277.192유한 상태 머신 형식 모델의 연구 동향

• 1277.193확률적 모델 검사의 최신 연구

• 1277.194파라메트릭 유한 상태 머신의 연구

• 1277.195하이브리드 오토마타와 유한 상태 머신의 결합

• 1277.196신경망 기반 상태 머신 추출 연구

• 1277.197형식 검증과 기계 학습의 융합 연구

• 1277.198유한 상태 머신 형식 모델의 한계와 확장 방향