본 논문은 사이버 물리 시스템의 실시간 동작을 지정하는 형식인 시간 제약 정규 표현식(Timed Regular Expressions)의 합성 문제를 다룬다. 양성 예제와 음성 예제를 모두 포함하는 주어진 시스템 동작 집합과 일치하는 시간 제약 정규 표현식을 생성하는 데 초점을 맞춘다. 단순한 시간 제약 정규 표현식을 탐색하여 합성 문제의 결정 가능성을 증명하고, 최소 길이를 갖는 일치하는 시간 제약 정규 표현식을 생성하는 방법을 제안한다. 이 방법은 후보 매개변수 시간 제약 정규 표현식을 열거하고 가지치기하는 단계와, 생성된 후보가 주어진 집합과 일치하는 요구 사항을 SMT(Satisfiability Modulo Theories) 공식으로 인코딩하여 매개변수 시간 제약 조건에 대한 해를 결정하는 단계로 구성된다. 마지막으로, 목표 시간 모델에서 무작위로 생성된 동작과 사례 연구를 포함한 벤치마크에서 제안된 방법을 평가한다.
