{"id":1115514,"date":"2025-01-02T15:04:08","date_gmt":"2025-01-02T23:04:08","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&#038;p=1115514"},"modified":"2025-01-02T15:04:09","modified_gmt":"2025-01-02T23:04:09","slug":"symbolic-automata-omega-regularity-modulo-theories","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/symbolic-automata-omega-regularity-modulo-theories\/","title":{"rendered":"Symbolic Automata: Omega-Regularity Modulo Theories"},"content":{"rendered":"<p>Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions and languages over finite words. In symbolic automata (or automata modulo <em>A<\/em>), an alphabet is represented by an effective Boolean algebra <em>A<\/em>, supported by a decision procedure for satisfiability. Regular languages over infinite words (so called \ud835\udf14-regular languages) have a rich history paralleling that of regular languages over finite words, with well-known applications to model checking via B\u00fcchi automata and temporal logics.<\/p>\n<p>We generalize symbolic automata to support \ud835\udf14-regular languages via <em>transition terms<\/em> and <em>symbolic derivatives<\/em>, bringing together a variety of classic automata and logics in a unified framework that provides all the necessary ingredients to support symbolic model checking modulo <em>A<\/em>. In particular, we define: (1) alternating B\u00fcchi automata modulo <em>A<\/em> (ABW\u27e8<em>A<\/em>\u27e9) as well (non-alternating) nondeterministic B\u00fcchi automata modulo <em>A<\/em> (NBW\u27e8<em>A<\/em>\u27e9); (2) an alternation elimination algorithm <strong>\u00c6<\/strong> that incrementally constructs an NBW\u27e8<em>A<\/em>\u27e9 from an ABW\u27e8<em>A<\/em>\u27e9, and can also be used for constructing the product of two NBW\u27e8<em>A<\/em>\u27e9; (3) a definition of linear temporal logic modulo <em>A<\/em>, LTL\u27e8<em>A<\/em>\u27e9, that generalizes Vardi\u2019s construction of alternating B\u00fcchi automata from LTL, using (2) to go from LTL modulo <em>A<\/em> to NBW\u27e8<em>A<\/em>\u27e9 via ABW\u27e8<em>A<\/em>\u27e9.<\/p>\n<p>Finally, we present RLTL\u27e8<em>A<\/em>\u27e9, a combination of LTL\u27e8<em>A<\/em>\u27e9 with extended regular expressions modulo <em>A <\/em>that generalizes the Property Specification Language (PSL). Our combination allows regex complement, that is not supported in PSL but can be supported naturally by using transition terms. We formalize the semantics of RLTL\u27e8<em>A<\/em>\u27e9 using the Lean proof assistant and formally establish correctness of the main derivation theorem.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions and languages over finite words. In symbolic automata (or automata modulo A), an alphabet is represented by an effective Boolean algebra A, supported by a decision procedure for satisfiability. Regular languages over [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13561,13560],"msr-publication-type":[193716],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-post-option":[269142],"msr-field-of-study":[246904,253147,253207,263617,251365],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-1115514","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-algorithms","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-post-option-include-in-river","msr-field-of-study-algorithm","msr-field-of-study-formal-specification","msr-field-of-study-regular-expression","msr-field-of-study-satisfiability-modulo-theories","msr-field-of-study-software-engineering"],"msr_publishername":"ACM","msr_edition":"","msr_affiliation":"","msr_published_date":"2025-1","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"ACM","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/01\/popl25-p11-final.pdf","id":"1115517","title":"popl25-p11-final","label_id":"243103","label":0},{"type":"doi","viewUrl":"false","id":"false","title":"10.1145\/3704838","label_id":"243106","label":0}],"msr_related_uploader":"","msr_attachments":[{"id":1115517,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2025\/01\/popl25-p11-final.pdf"}],"msr-author-ordering":[{"type":"user_nicename","value":"Margus Veanes","user_id":32806,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Margus Veanes"},{"type":"user_nicename","value":"Thomas Ball","user_id":33895,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Thomas Ball"},{"type":"user_nicename","value":"Gabriel Ebner","user_id":42573,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Gabriel Ebner"},{"type":"text","value":"Ekaterina Zhuchko","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[199565],"msr_event":[],"msr_group":[144812],"msr_project":[259698],"publication":[],"video":[],"download":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":259698,"post_title":"Automata","post_name":"automata","post_type":"msr-project","post_date":"2016-07-20 18:35:07","post_modified":"2018-12-04 17:02:22","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/automata\/","post_excerpt":"Automata is a .NET library that provides algorithms for composing and analyzing regular expressions, automata, and transducers. In addition to classical word automata, it also includes algorithms for analysis of tree automata and tree transducers. The library covers algorithms over finite alphabets as well as their symbolic counterparts. In symbolic automata concrete characters have been replaced by character predicates. Such predicates can range over very large or even infinite alphabets, like integers. Predicates can be&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/259698"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1115514","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1115514\/revisions"}],"predecessor-version":[{"id":1115520,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/1115514\/revisions\/1115520"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=1115514"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=1115514"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=1115514"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=1115514"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=1115514"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=1115514"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=1115514"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=1115514"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=1115514"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=1115514"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=1115514"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=1115514"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=1115514"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=1115514"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=1115514"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=1115514"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}