\documentclass[runningheads]{llncs}

\usepackage[T1]{fontenc}

%\pagestyle{plain}
% \usepackage{todonotes}
\usepackage[toc,page]{appendix}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{url}
\usepackage[dvipsnames]{xcolor}

\urldef{\mailsa}\path|{alfred.hofmann, ursula.barth, ingrid.haas, frank.holzwarth,|
\urldef{\mailsb}\path|anna.kramer, leonie.kunz, christine.reiss, nicole.sator,|
\urldef{\mailsc}\path|erika.siebert-cole, peter.strasser, lncs}@springer.com|
% \newcommand{\keywords}[1]{\par\addvspace\baselineskip
% \noindent\keywordname\enspace\ignorespaces#1}

% \usepackage{breqn}
\usepackage{tabularx}
\usepackage{booktabs}
\usepackage{multirow}
\usepackage{multicol}
\usepackage{hhline}
\usepackage[inline]{enumitem}
\usepackage[normalem]{ulem}

\usepackage[utf8]{inputenc}
\usepackage{graphicx}
\usepackage{xspace}
\usepackage[noend,vlined,ruled,boxed,linesnumbered]{algorithm2e}
\newcommand\mycommfont[1]{\footnotesize\ttfamily\textcolor{blue}{#1}}
\SetCommentSty{mycommfont}
\usepackage{algorithmic}
\usepackage{hyperref}
\usepackage{amsmath}%
% \usepackage{subfig} % two figure in one column
% correct bad hyphenation here
\usepackage{wrapfig}
\usepackage{caption}
\usepackage{cite}
%% math font
\usepackage{mathrsfs}
% \usepackage{times} 
%\usepackage{savetrees}

\usepackage{enumitem}
\setlist[itemize]{noitemsep, nolistsep, topsep=0pt, partopsep={0pt}}

\usepackage{pgfplots}
\pgfplotsset{compat=1.9}

% We will externalize the figures
% If CAV2024/ToolPaper-figure0.pdf does not exists, MUST RUN WITH 
% "pdflatex -shell-escape" OR "latexmk -shell-escape"
\usepgfplotslibrary{external}
\tikzexternalize

% lstlisting
\usepackage{listings}

% while this toolchain supports full end-to-end translation, none of the hwmcc20 solvers we target accept fair properties, and therefore do not output inifinte traces

% \usepackage[firstpage]{draftwatermark}

\definecolor{gray}{RGB}{102,102,102}		%#666666
\definecolor{lightblue}{RGB}{0,102,153}		%#006699
\definecolor{lightgreen}{RGB}{102,153,0}	%#669900
\definecolor{bluegreen}{RGB}{51,153,126}	%#33997e
\definecolor{magenta}{RGB}{217,74,122}		%#d94a7a
\definecolor{orange}{RGB}{226,102,26}		%#e2661a
\definecolor{purple}{RGB}{ 171, 15, 247 }		%#7d4793
\definecolor{codegreen}{RGB}{113,138,98}		%#718a62
\definecolor{codered}{RGB}{ 220, 43, 15 }
\definecolor{codeblue}{RGB}{ 15, 86, 220 }

\lstdefinelanguage{MoXI}
{
  morekeywords = [1]{define-system,check-system,define-fun,check-system-response,set-logic,declare-enum-sort,let},
  morekeywords = [2]{
  :assumption,
  :certificate,
  :current,
  :init,
  :input,
  :inv,
  :lasso,
  :local,
  :model,
  :output,
  :prefix,
  :reachable,
  :result,
  :query,
  :subsys,
  :trace,
  :trail,
  :trans
  },
  morekeywords = [3]{Bool,Int,BitVec,Array},
  morekeywords = [4]{},
  %function1
  keywordstyle = [1]\color{purple},
  keywordstyle = [2]\color{codeblue},
  keywordstyle = [3]\color{codered},
  keywordstyle = [4]\color{magenta},
  sensitive = true,
  % list of keywords
  sensitive=true, % keywords are not case-sensitive
  morecomment=[l]{;}, % l is for line comment
  extendedchars=true,
  alsoletter={-,:},
}

\lstdefinelanguage{SMV}
{
  morekeywords = [1]{MODULE,State:,Input:},
  morekeywords = [2]{unsigned,word},
  morekeywords = [3]{INIT,TRANS,INVAR,IVAR,VAR,INVARSPEC},
  morekeywords = [4]{},
  %function1
  keywordstyle = [1]\color{purple},
  keywordstyle = [2]\color{codered},
  keywordstyle = [3]\color{codeblue},
  keywordstyle = [4]\color{magenta},
  sensitive = true,
  % list of keywords
  sensitive=true, % keywords are not case-sensitive
  morecomment=[l]{--}, % l is for line comment
  extendedchars=true,
  alsoletter={-,:},
}

\lstdefinestyle{mystyle}{
    % backgroundcolor=\color{backcolour},   
    commentstyle=\color{codegreen},
    keywordstyle=\color{magenta},
    numberstyle=\tiny\color{gray},
    stringstyle=\color{purple},
    basicstyle=\fontsize{8}{9}\ttfamily,
    breakatwhitespace=false,         
    breaklines=false,                 
    captionpos=b,                    
    keepspaces=true,                 
    numbers=left,                    
    numbersep=5pt,                  
    showspaces=false,                
    showstringspaces=false,
    showtabs=false,                  
    tabsize=2,
    escapeinside={/*!}{!*/},
}

\lstset{style=mystyle}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Figure Magic
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\usepackage{epsfig}
\usepackage{float} % put figure in minipage
%\usepackage{framed}
%\usepackage{subfigure}

% diagonal line in the table
\usepackage{diagbox}

\usepackage{enumitem}
\newlist{Properties}{enumerate}{2}
\setlist[Properties]{label=Property \arabic*.,itemindent=*}

\usepackage{tikz}
\newcommand*\circled[1]{\tikz[baseline=(char.base)]{
            \node[shape=circle,draw,inner sep=2pt] (char) {#1};}}

\newcommand{\VarPhiSequence}{\ensuremath{\langle T_{\varphi} \rangle}\xspace}
\newcommand{\ExSeq}[1]{\ensuremath{\langle T_{#1} \rangle}\xspace}
\newcommand{\ExSeqElement}[2]{\ensuremath{\langle T^{#1}_{#2} \rangle}\xspace}
\newcommand{\IN}{\mathbb{N}}
\newcommand{\cb}[1]{\textcolor{blue}{#1}}
% draw box around text
\usepackage{tcolorbox}

\renewcommand{\topfraction}{.99} %figures can take up at most 99% of the page before being alone
\renewcommand{\bottomfraction}{.99} %figures can take up at most 99% of the page before being alone
\renewcommand{\textfraction}{.01} %at most this % of page will be text before making figure-only page
\addtolength{\textfloatsep}{-5mm}
\addtolength{\floatsep}{-5mm}
\addtolength{\intextsep}{-5mm}
\addtolength{\abovecaptionskip}{-4mm}
%\addtolength{\belowcaptionskip}{-2mm}

\newcommand{\reqUnobtrusiveness}{\textsc{Unobtrusiveness}\xspace}
\newcommand{\reqResponsiveness}{\textsc{Responsiveness}\xspace}
\newcommand{\reqRealizability}{\textsc{Realizability}\xspace}
\newcommand{\reqUnobtrusive}{\textsc{Unobtrusive}\xspace}
\newcommand{\reqResponsive}{\textsc{Responsive}\xspace}
\newcommand{\reqRealizable}{\textsc{Realizable}\xspace}

\newcommand{\true}{\texttt{true}\xspace}
\newcommand{\false}{\texttt{false}\xspace}

\newcommand{\nuxmvmcil}{\textsc{nuxmv2mcil}\xspace}
\newcommand{\mcilbtor}{\textsc{mcil2btor}\xspace}
\newcommand{\btorwitmcilwit}{\textsc{btorwit2mcilwit}\xspace}
\newcommand{\mcilwitnuxmvwit}{\textsc{mcilwit2nuxmvwit}\xspace}
\newcommand{\sortcheck}{\textsc{sortcheck}\xspace}
\newcommand{\validate}{\textsc{validate}\xspace}
\newcommand{\catbtor}{\textsc{catbtor}\xspace}
\newcommand{\btormc}{\textsc{BtorMC}\xspace}
\newcommand{\avr}{\textsc{AVR}\xspace}
\newcommand{\nuXmv}{\textsc{nuXmv}\xspace}
\newcommand{\aiger}{\textsc{Aiger}\xspace}
\newcommand{\btor}{\textsc{Btor2}\xspace}
\newcommand{\btortools}{\textsc{Btor2Tools}\xspace}
\newcommand{\moxi}{\textsc{MoXI}\xspace}
\newcommand{\pono}{\textsc{Pono}\xspace}

\def\<{{\langle}}
\def\>{{\rangle}}
\def\:{{\colon}}
\def\ltl{{\sf LTL}\xspace}
\def\U{{\mathcal{U}}}
\def\R{{\mathcal{R}}}
\newtheorem{Def}{Definition}
\renewcommand{\phi}{\varphi}

% \usepackage{showframe} 

% \usepackage[font=small,labelfont=bf]{caption}

\hypersetup{
    colorlinks=true,
    linkcolor=blue,
    filecolor=magenta,      
    citecolor=gray,      
    urlcolor=cyan,
    pdftitle={\moxi: An Intermediate Language for Symbolic Model Checking},
    }

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{ %
  \moxi: An Intermediate Language \\ for Symbolic Model Checking %The Symbolic Model-Checking Intermediate Language
  \thanks{This work was funded by NSF:CCRI Award \#2016592, \#2016597, \#2016656. The GitHub organization provides full artifacts: \url{ https://github.com/ModelChecker}. Thanks to our international Technical Advisory Board for invaluable feedback; see the project website: \url{https://modelchecker.temporallogic.org}.} %\vspace{-0.1in}
}%
% \vspace{-0.2in} %
% \author{}
% \institute{}
% a short form should be given in case it is too long for the running head
\titlerunning{\moxi: An Intermediate Language for Symbolic Model Checking}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%

\author{Kristin Yvonne Rozier\inst{1}, Rohit Dureja\inst{2}, Ahmed Irfan\inst{3}, Chris Johannsen\inst{1}, Karthik Nukala\inst{3}, Natarajan Shankar\inst{3}, Cesare Tinelli\inst{4}, Moshe Y. Vardi\inst{5}}
%\authorrunning{All of us}
\institute{Iowa State University \{kyrozier, cgjohann\}@iastate.edu \and Advanced Micro Devices, Inc. (rohit.dureja@amd.com) \and SRI International \{karthik.nukala, ahmed.irfan, shankar\}@sri.com \and The University of Iowa (cesare-tinelli@uiowa.edu) \and Rice University (vardi@cs.rice.edu)}
%
\authorrunning{K.~Y.~Rozier et al.}

%--------------------------------------------------
%Keywords: 
%--------------------------------------------------


%passes
% NB: a more complex sample for affiliations and the mapping to the
% corresponding authors can be found in the file "llncs.dem"
% (search for the string "\mainmatter" where a contribution starts).
% "llncs.dem" accompanies the document class "llncs.cls".
%

% \toctitle{Lecture Notes in Computer Science}
% \tocauthor{Authors' Instructions}
\maketitle

% \SetWatermarkAngle{0}
%%%%%%%%% Use only one of the four following blocks
% use this block if you received the the "reusable" badge
% \SetWatermarkText{\raisebox{10.5cm}{%
%   \hspace{0.1cm}%
%   \href{https://doi.org/10.5281/zenodo.7889284}{\includegraphics{figs/1-available}}% 
%   \hspace{9cm}%
%   \includegraphics{figs/3-reusable}%
% }}

% CONTRIBUTIONS:
% 1. Language
% 2. Tool suite
%   2a. Translation framework
%   2b. Tool validation
%   2c. Benchmark set
% 3. Tool evaluation

%\vspace{-.2in}
\begin{abstract}
  Three progressive challenges stand in between the popular, ``push-button,'' industrially valuable technique of symbolic model checking and the level of widespread adoption achieved by other verification techniques: (1) the specification bottleneck; (2) the state-space explosion problem; and (3) the lack of standardization and open-source implementations limiting the impact of advances in (1) and (2). We address this third challenge. Learning from past definitions of intermediate languages and common interfaces, as well as input from the international research community, we define a new, extensible intermediate language %as a standard interface
  for hardware symbolic model checking. 
  Our contributions include: (a) defining the syntax and semantics of {\bf \moxi}, the
  {\bf Mo}del e{\bf X}change {\bf I}nterlingua
  %new symbolic model-checking intermediate language
  designed to become a standard for the international research community; (b) demonstrating that an initial implementation of symbolic model checking through \moxi performs competitively with current state-of-the-art symbolic model checkers; (c) reframing the next symbolic model checking research challenges considering this new community standard.

%\vspace{-0.1in}
\keywords{Model Checking  \and Intermediate Language \and SMT.}
\end{abstract}



\section{Introduction}\label{sec:intro}

%%CT I have slightly modified the text in a few places in this section to make it read less confrontational

Symbolic model checking has made foundational changes to impactful, real-world system designs, yet its ascent to a common-place verification technique is currently most limited by a few barriers to adoption, centering on its lack of standardization. For just one example, in our own work, symbolic model checking with \nuXmv pinpointed hard-to-find, requirements-violating control sequences, and thus changed the design of NASA's Automated Airspace Concept \cite{ZR12,ZR14}. This led to NASA using \nuXmv for the next, much larger, stages of the project, including model checking with fault-tree analysis of a large set of possible safe configurations of the next-generation system \cite{MCGTR15}, and design-space exploration of over 20,000 possible air traffic control designs \cite{GCMTR16}. 

The collection of impactful success stories of symbolic model checking in real-world system development are far too many and too diverse to cite in a single paper; there is no question that model checking provides value beyond its cost in verifying a wide range of systems uphold requirements for safety, security, and other desirable properties (such as consistency or financial soundness). However, model checking is still not as commonly-used as informal verification techniques such as simulation and testing. One primary reason for this is the specification bottleneck \cite{Roz16}: creating and validating system models and temporal logic specifications remains a challenging undertaking. The second barrier to adoption is the famous state-space explosion problem: the combination of the modeling technique used to represent the relevant system characteristics and the back-end model-checking algorithm can result in an untenable search space. However, the third barrier is perhaps both the broadest impediment and the easiest to overcome: a lack of standardization in symbolic model checking prevents the propagation of techniques aimed at lowering to the first two barriers.

The SMV modeling language represents an advancement in ameliorating barrier (1), the specification bottleneck: it is an expressive modeling language that, due to its appealing syntax that intuitively represents many common systems, continues to be successfully used in a wide range of industrial verification efforts \cite{RLS02,GHBTCM02,TM03,CH03,MTWH06,Mil08,YJC09,BCKNNR09,GDH11,LVBFNH12,BCFJKPRT15,ZR12,ZR14,MCGTR15,GCMTR16,DRR17,DR17}. Two freely-available model checkers previously provided viable research platforms for checking SMV language models: CadenceSMV \cite{McM93} and \textsc{NuSMV} \cite{CCGGPRST02} (which is integrated into today’s \nuXmv \cite{nuxmv}). Yet, today CadenceSMV's 32-bit pre-compiled binary and \nuXmv's increasingly restricted, closed-source releases are no longer suitable for research, e.g., into improved model-checking algorithms. How can we continue the progression of high-level language model checking in SMV with no open-source research platforms that allow new algorithms under the hood, e.g., to continue mitigating the state-space explosion problem?

%SMV as a modeling language is important because it has significantly reduced the (first) specificaion barrier. Uniquely from other model-checking input languages, it includes high-level constructs critically required for modeling and validating safety-critical systems, such many aerospace operational systems, from Boeing's Wheel Braking System \cite{BCFJKPRT15} to NASA's Automated Airspace Concept \cite{ZR12,ZR14,MCGTR15,GCMTR16} to a variety of Unmanned Aerial Systems \cite{SRRMMI13,RRS14}. SMV has been used widely by the hardware model checking community as well (e.g., at FMCAD \cite{FMCAD}) and has appealing qualities that could further widespread integration of formal methods, yet we cannot ........... second baarrier


\begin{wrapfigure}{r}{0.6\textwidth}
	\centering
	\vspace{-0.2in}
        \includegraphics[width=0.58\textwidth]{../figs/heuristics_time.pdf}
	%\vspace{-0.3in}
    \caption{FuseIC3\cite{DR17}: model checking \textcolor{OliveGreen}{\bf 34 formulas} over \textcolor{RedViolet}{\bf 1,620 models} is \textcolor{red}{\bf 5.48x faster.}}
	%\vspace{-0.2in}
    \label{fig:FuseIC3}
    %\vspace{0.1in}
\end{wrapfigure}
Continuing with our example of symbolic model checking in NASA's next-generation transportation system, the next step of the process was to narrow down the design space (system designers reduced the possible configurations from 20,250 to 1,620), add details, and continue design-space model checking to refine the (safe) design set. To improve performance (per barrier (2), the state space explosion problem), we designed a new algorithm for model checking large design spaces, FuseIC3 \cite{DR17}. However, to compare FuseIC3 with the state-of-the-art symbolic model-checking algorithms (namely, those claimed to be used in \nuXmv \cite{EMB11} and in industry \cite{BBEL96}), we had to {\bf re-implement both of these existing model checkers from scratch} --- our results appear in Figure \ref{fig:FuseIC3}. In other words, there was no easy way to compare state-of-the-art model checking back-end algorithms because the existing implementations were closed source, and did not check models in the same modeling languages. No tool accepted our SMV-language models and implemented the best back-end model-checking algorithm for the industrial verification task at hand, and there was no way to add additional algorithms to \nuXmv because it is closed source. (It would also have been useful to check how closely \nuXmv implemented the state-of-the-art algorithms described in the literature, and to be able to modify the existing implementation.) In addition to being a time-consuming engineering task, this hurdle also curtailed the use of model checking in this NASA project. The lack of standardization in symbolic model checking meant that it was no longer the case that the benefits of model checking outweighed the cost. While we successfully ameliorated barriers (1) and (2), at least in the context of the task at hand, we could not apply our advances efficiently, or in the context of existing, and trusted, model-checking infrastructures. 

This is not a unique story. The Hardware Model Checking Competition (HWMCC) \cite{hwmcc20} regularly spurs back-end algorithmic advances in symbolic model checking. However, the competing tools historically only accepted models in the bit-level input language \aiger \cite{aigerformat,aigerformatupdate}; HWMCC only recently advanced to the word-level, yet still machine-oriented, language \btor~\cite{NPWB2018}. Such languages do not support direct modeling of modern complex systems --- the way SMV does --- and hinder adoption; it is very hard to convince industrial system designers that \aiger or \btor models correctly capture their higher-level systems. 
Most existing pathways for translating from high-level models to \aiger or \btor focus on hardware designs, and do not provide a natural means to describe realistic systems. Even outside of HWMCC, many new, advanced, model-checking algorithms get developed for open-source, award-winning, model-checking engines, like ABC~\cite{brayton2010abc}, which do not accept models in popular languages that would benefit from model checking using those algorithms. Then, we also face the open problem of translating counterexamples produced, e.g., by ABC, back into meaningful counterexamples for a non-hardware-centric higher-level language model, such as a model in SMV.

For another example, the PANDA algorithm and tool achieved up to exponential performance improvement using the same symbolic model-checking back-end, just by encoding LTL input specifications differently \cite{RV11}. Yet PANDA's impact is limited since the implementation is only compatible with tools that accept models written in SMV. If, instead, PANDA translated LTL specifications into a common intermediate language, we could use it to improve model-checking performance broadly. 

%\subsection{\moxi}

To alleviate the language issues above
we introduce {\bf Model Exchange Interlingua (\moxi)}, an intermediate language meant to be a common input and output standard for model checkers for finite- and infinite-state systems. %, with an initial focus is on finite-state ones.
%
\moxi was designed to be general enough to be an intermediate target language for a variety of user-facing specification languages for model checking. At the same time, \moxi is simple enough to be easily comparable to lower-level languages or be directly supported by model-checking tools based on SAT/SMT technology.

%
Models expressed in \moxi are expected to be produced and processed by tools. Thus \moxi provides: a simple, easily-machine-parsable syntax; a rich set of data types; minimal syntactic sugar (at least initially); a well-understood formal semantics; a small but comprehensive set of commands; and simple translations to lower-level modeling languages, such as \btor~\cite{NPWB2018}.
Based on these principles, \moxi does not provide direct support for many of the expressive features offered by current hardware modeling languages such as VHDL\cite{IEEE93,IEEE19} and Verilog\cite{IEEE05}, or more general-purpose system modeling languages such as SMV\cite{McM99,CCJKOPRT05}, TLA+\cite{Lam02}, PROMELA\cite{Hol03}, Simulink\cite{simulink}, SCADE\cite{CPP17,scade}, and Lustre\cite{CPHP87,JRH16}. However, it is sufficiently expressive that problems defined in reasonably large fragments of those languages can be reduced to problems in \moxi.
%
\moxi closely resembles the SMT-LIB language \cite{SMTLib,BarST-SMT-10}, but with new commands to define and verify systems. It allows the definition of multi-component synchronous or asynchronous reactive systems. It also allows the specification and checking of reachability conditions (or, indirectly, state and transition invariants) and deadlocks, possibly under fairness conditions on input values.


%%KYR: moving this bit to the moxi definition later...
%% \moxi assumes a discrete and linear notion of time and hence has a standard trace-based semantics. Each system definition:

%% \begin{itemize}
%% \item defines a \emph{transition system} via the use of SMT formulas, imposing minimal syntactic restrictions on those formulas;
%% \item is parametrized by a \emph{state signature}, a sequence of typed variables;
%% \item partitions state variables into input, output and local variables;
%% \item can be expressed as the synchronous or asynchronous composition of other systems
%% \item is \emph{hierarchical}, i.e., may include (instances of) previously defined systems as subsystems;
%% \item can encode both synchronous and asynchronous system composition.
%% \end{itemize}

% The current focus on _finite-state_ systems. However, the language has been designed to support the specification of infinite-state system as well.

%(Mention the Verilog to SMV to IL to BTOR path?)

With \moxi, it is now possible to introduce or refine expressive modeling languages, model check them using existing and future state-of-the-art back-end algorithms, and return counterexamples in the original, high-level modeling language, simply by creating a translation between the modeling language and \moxi. Advances in back-end model checking algorithms can now be leveraged for models in any number of high-level modeling languages, simply by creating a translation between their low-level representations and \moxi. Most
importantly, innovations mitigating the specification bottleneck and the
state-space explosion problem will now push forward symbolic model checking as a whole, rather than advancing a single tool. 


We introduce the notation and trace semantics underlying \moxi in Section~\ref{sec:preliminaries}. Section~\ref{sec:moxi} defines \moxi, including the semantics for system definition and system checking. We demonstrate a prototype implementation translating the SMV modeling language through \moxi for model checking with the top tools from the last HWMCC in Section~\ref{sec:translator}. 
Section~\ref{sec:discussion} concludes with a concrete list of future research directions for the international symbolic model checking community, given the standardization provided by \moxi.

\section{Preliminaries}\label{sec:preliminaries}
%\vspace{-0.1in}

The base logic of \moxi is the same as that of SMT-LIB: many-sorted first-order logic with equality and \texttt{let} binders. We refer to this logic simply as FOL. When we say \emph{formula}, with no further qualifications, we refer to an arbitrary formula of FOL (possibly with quantifiers and \texttt{let} binders).

We say that a formula is \emph{quantifier-free} if it contains no occurrences of the quantifiers $\forall$ and $\exists$. We say that it is \emph{binder-free} if it is quantifier-free and also contains no occurrences of the \texttt{let} binder. The \emph{scope} of binders and the notion of \emph{free} and \emph{bound} (occurrences of) variables in a formula are defined as usual.

\subsection{Notation}

If $F$ is a formula and $\boldsymbol{x} = (x_1, \ldots, x_n)$ a tuple of distinct variables, we write $F[\boldsymbol{x}]$ or $F[x_1, \ldots, x_n]$ to express the fact that every variable in $\boldsymbol{x}$ occurs free in $F$ (although $F$ may have additional free variables). Let $\sigma(x_i)$ denote the type or \emph{sort} of variable $x_i$ in $\boldsymbol{x}$. We denote by $\boldsymbol{x'}$ the tuple $(x_1',\ldots,x_n')$ such that $\sigma(x_i) = \sigma(x_i')$. We write $\boldsymbol{x}, \boldsymbol{y}$ to denote the concatenation of tuple $\boldsymbol{x}$ with tuple $\boldsymbol{y}$. When it is clear from the context, given a formula $F[\boldsymbol{x}]$ and a tuple $\boldsymbol{t} = (t_1, \ldots, t_n)$ of terms of the same type as $\boldsymbol{x} = (x_1, \ldots, x_n)$, we write $F[\boldsymbol{t}]$ or $F[t_1, \ldots, t_n]$ to denote the formula obtained from $F$ by simultaneously replacing each occurrence of $x_i$ by $t_i$ for all $i=1,\ldots,n$.
%
A formula may contain \emph{uninterpreted} constant and function symbols, that is, symbols with no constraints on their interpretation. For most purposes, we treat uninterpreted constant and function symbols as free (rigid) variables 
respectively of first and second order.

\begin{definition}[Transition system]
A transition system $S$ is a pair of predicates of the form $S = (I_S [\boldsymbol i, \boldsymbol o,  \boldsymbol l],~T_S [\boldsymbol i, \boldsymbol o, \boldsymbol l, \boldsymbol{i'}, \boldsymbol{o'}, \boldsymbol{l'}]
)$
where\vspace{-0.1in}
\begin{enumerate}%[label=\emph{\bf(\arabic*)}]
\item $\boldsymbol i$ and $\boldsymbol{i'}$ are tuples of \emph{input variables};
\item $\boldsymbol o$ and $\boldsymbol{o'}$ are tuples of \emph{output variables};
\item $\boldsymbol l$ and $\boldsymbol{l'}$ are tuples of \emph{local variables};
\item $I_S$ is a formula representing the \emph{initial state condition}; and% expressed as a formula with no (free) variables from $\boldsymbol{i'}$, $\boldsymbol{o'}$, and $\boldsymbol{l'}$;
\item $T_S$ is a formula representing the \emph{transition condition}. %, expressed as a formula over the variables $\boldsymbol{i}$, $\boldsymbol{o}$, $\boldsymbol{l}$,$\boldsymbol{i'}$, $\boldsymbol{o'}$, and $\boldsymbol{l'}$.
\end{enumerate}
\end{definition}

\subsection{Trace Semantics}

A transition system implicitly defines a model (i.e., a Kripke structure) of First-Order Linear Temporal Logic (FO-LTL). The language of FO-LTL extends that of FOL with the same modal operators of time as in standard (propositional) LTL:
$\mathbf{always},$
$\mathbf{eventually},$
$\mathbf{next},$
$\mathbf{until},$
$\mathbf{release}$.
For our purposes of defining the semantics of transition systems, it is enough to consider just the $\mathbf{always}$ and $\mathbf{eventually}$ operators.

The set of non-temporal operators depends on the particular theory, in the sense of SMT, considered (e.g., linear integer/real arithmetic, bit vectors, strings, and so on, and their combinations).
The meaning of theory symbols (such as arithmetic operators) and theory sorts (such as $\mathsf{Int}$,
$\mathsf{Real},$
$\mathsf{Array(Int, Real)},$
$\mathsf{BitVec(3)}$, $\ldots$)
is fixed by the theory $\mathcal T$. With a fixed theory $\mathcal T$, the meaning of a FO-LTL formula $F$ is provided by an interpretation of the uninterpreted (constant and function) symbols of $F$, if any, as well as an infinite sequence of valuations for the free variables of $F$.

Let tuple $\boldsymbol x = (x_1,\ldots,x_n)$ denote distinct \emph{state} variables, meant to represent the state of a computation system. We write formulas of the form $F[\boldsymbol f, \boldsymbol x, \boldsymbol x']$ where $\boldsymbol f$ is a tuple of uninterpreted (constant and function) symbols. If $F$ has free occurrences of variables from $\boldsymbol x$ but not from $\boldsymbol{x'}$ we call it a \emph{one-state} formula; otherwise, we call it a \emph{two-state} formula.

A \emph{valuation} of $\boldsymbol x$, or a \emph{state over} $\boldsymbol x$, is a function mapping each variable $x$ in $\boldsymbol x$ to a value of $x$'s sort. Let $\kappa$ be a positive ordinal up to $\omega$, the cardinality of the natural numbers.
A \emph{trace} (of length $\kappa$ over $\boldsymbol x$) is any state sequence $\pi = (s_j  \mid 0 \leq j < \kappa)$. Note that $\pi$ is the finite sequence $s_0, \ldots, s_{\kappa-1}$ when $\kappa < \omega$, and is the infinite sequence $s_0, s_1, \ldots$ otherwise. 
For all $i$ such that $0 \leq i < \kappa$, we denote by $\pi[i]$ the state $s_i$ and by $\pi^i$ the subsequence $(s_j \mid i \leq j < \kappa)$.

\paragraph{\bf Infinite trace semantics}

Let $F[\boldsymbol f, \boldsymbol x, \boldsymbol{x'}]$ be a formula as above.
If $\mathcal I$ is an interpretation of $\boldsymbol{f}$ in the theory $\mathcal T$ and $\pi$ is an infinite trace, then $(\mathcal I, \pi)$ \emph{satisfies} $F$, written $(\mathcal I, \pi) \models F$, \emph{iff} one of the following holds:
\vspace{-0.1in}
\begin{enumerate}
\item $F$ is atomic and
  $\mathcal{I}[\boldsymbol x \mapsto \pi[0](\boldsymbol x),\boldsymbol{x'} \mapsto \pi[1](\boldsymbol x)]$
  satisfies $F$ as in FOL;
\item $F = \lnot G~$ and
  $~(\mathcal I, \pi) \not\models G$;
\item $F = G_1 \land G_2~$ and
  $~(\mathcal I, \pi) \models G_i$ for $i=1,2$;
\item $F = \exists z\, G$ and
  $(\mathcal I[z \mapsto v], \pi) \models G$ for some value $v$ for $x$;
\item $F = \mathbf{eventually}~G$ and
  $(\mathcal I, \pi^i) \models G$ for some $i \geq 0$;
\item $F = \mathbf{always}~G$ and
  $(\mathcal I, \pi^i) \models G$ for all $i \geq 0$.
\end{enumerate}

The semantics of the propositional connectives $\lor, \rightarrow, \leftrightarrow$, and the quantifier $\forall$ can be defined by reduction to the connectives above (e.g., by defining $G_1 \lor G_2$ as $\lnot(\lnot G_1 \land \lnot G_2)$, and so on). Note that $\exists z$ is a \emph{static}, or \emph{rigid}, quantifier: the meaning of the variable it quantifies does not change over time, i.e., from state to state in $\pi$.
Uninterpreted symbols are rigid in the same sense: their meaning does not change over time.\footnote{Another way to understand the difference between rigid and non-rigid symbols is that state variables are mutable over time, whereas quantified variables, theory symbols, and uninterpreted symbols are all immutable.}
%
Given a transition system $S = (I_S, T_S)$,
% state variables $\boldsymbol i, \boldsymbol o,  \boldsymbol l$, such that
% $$S = (I_S [\boldsymbol i, \boldsymbol o,  \boldsymbol l],~
%        T_S [\boldsymbol i, \boldsymbol o, \boldsymbol l, \boldsymbol{i'}, \boldsymbol{o'}, \boldsymbol{l'}]
% )$$
the infinite trace semantics of $S$ is the set of all pairs $(\mathcal I, \pi)$ of interpretations $\mathcal I$ in $\mathcal T$ and infinite traces $\pi$ such that $(\mathcal I, \pi) \models I_S \land\ \mathbf{always}~T_S$. We call any such pair an \emph{execution of $S$}.

\paragraph{\bf Finite trace semantics}
Given formula $F[\boldsymbol f, \boldsymbol x, \boldsymbol{x'}]$, interpretation $\mathcal I$ in theory $\mathcal T$, infinite trace $\pi$, and $n \geq 0$, 
$(\mathcal I, \pi)$ $n$-\emph{satisfies} $F$, written $(\mathcal I, \pi) \models_n F$, \emph{iff}
\vspace{-0.1in}
\begin{enumerate}
\item $F$ is atomic and $\mathcal I[\boldsymbol x \mapsto \pi[0](\boldsymbol x), \boldsymbol{x'} \mapsto \pi[1](\boldsymbol x)]$ satisfies $F$ as in FOL;

\item $F = \lnot G$ and $(\mathcal I, \pi) \not\models_n G$;

\item $F = G_1 \land G_2$ and $(\mathcal I, \pi) \models_n G_i$ for $i=1,2$;

\item $F = \exists z\, G$ and $(\mathcal I[z \mapsto v], \pi) \models_n G$ for some value $v$ for $z$;

\item $F = \mathbf{eventually}~G$ and $(\mathcal I, \pi^i) \models_{n-i} G$ for some $i = 0, \ldots, n$; or

\item $F = \mathbf{always}~G$ and $(\mathcal I, \pi^i) \models_{n-i} G$ for all $i = 0, \ldots, n$.
\end{enumerate}

The semantics of the propositional connectives $\lor, \rightarrow, \leftrightarrow$, and the quantifier $\forall$ is defined by reduction to the connectives above.
Intuitively, $n$-satisfiability specifies when a formula is true over a trace's first $n$ states.
Note that this notion is well defined even when $n=0$ regardless of whether $F$ has free occurrences of variables from $\boldsymbol{x'}$ or not.
This is true in the atomic case because the infinite trace $\pi$ contains the state $\pi[1]$.
The claim can be shown in the general case by a simple inductive argument.

The notion of $n$-satisfiability is useful in state reachability.
A state satisfying a (non-temporal) state property $R$ is reachable in a system $S$ only if the temporal formula $\mathbf{eventually}~R$ is $n$-satisfied by an execution of $S$ for some $n$.
Note that the converse does not hold; $R$ can be reachable in a system $S$ without being $n$-satisfied by an execution of $S$.

\section{The \moxi Intermediate Language}\label{sec:moxi}

\moxi assumes a discrete and linear notion of time and adopts the trace-based semantics defined in the previous section. 
It builds on the SMT-LIB language, extending it with commands to represent transition systems and to specify properties or \emph{queries}.
It also standardizes a format for witnesses generated by back-end algorithms. Table \ref{tbl:smtlib_cmd} shows the supported SMT-LIB commands in \moxi. Since enumerated sorts are useful in modeling real-world systems, \moxi introduces a \texttt{declare-enum-sort} command. For example, \texttt{(declare-enum-sort $s$ ($c_1$ $\cdots$ $c_n$ ))} declares $s$ to be an enumerative type with (distinct) values $c_1, \ldots, c_n$.


\begin{table}
\vspace{-0.1in}
  \begin{center}
\caption{Supported SMT-LIB commands in \moxi}
\label{tbl:smtlib_cmd}
\begin{tabular}{p{0.9\linewidth}}
% Command & Intent  \\
\hline
\texttt{(declare-sort $s$ $n$)}

Declares $s$ to be a sort symbol (i.e., type constructor) of arity $n$.  \\ \hline

\texttt{(define-sort $s$ ($u_1$ $\cdots$ $u_n$) $\tau$)}

Defines $S$ as a synonym of a parametric type $\tau$ with parameters $u_1 \cdots u_n$. \\ \hline

\texttt{(declare-const $c$ $\sigma$)}

Declares a constant $c$ of sort $\sigma$. \\ \hline

\texttt{(define-fun $f$ ( ( $x_1$ $\sigma_1$ ) $\cdots$ ( $x_n$ $\sigma_n$ ) ) $\sigma$ $t$)}

Defines a function $f$ with inputs $x_1, \ldots, x_n$ (of respective sort $\sigma_1, \ldots, \sigma_n$), output sort $\sigma$, and body $t$. \\ \hline
\texttt{(set-logic $L$)} 

Defines the model's \emph{data logic}, i.e., the background theories of relevant data types (e.g., integers, reals, bit vectors, and so on) as well as the language of allowed logical constraints (e.g., quantifier-free, linear, etc.). \\ \hline

% \texttt{(declare-enum-sort $s$ ( $c_1$ $\cdots$ $c_n$ ) )}

% Declares $s$ to be an enumerative type with (distinct) values $c_1, \ldots, c_n$. \\ \hline
\end{tabular}
\end{center}
\vspace{-0.2in}
\end{table}

\subsection{System Definition}
\moxi allows the definition of a model 
as the composition of one or more \emph{systems}.
 \moxi’s system definition commands follow the SMT-LIB syntax 
for attribute-value pairs.
Each system definition:
%\vspace{-0.1in}
\begin{enumerate}
\item defines a \emph{transition system} via the use of SMT formulas, imposing minimal syntactic restrictions on those formulas;
\item is parameterized by a \emph{state signature}, a sequence of typed variables;
\item partitions \emph{state} variables into \emph{input}, \emph{output}, and \emph{local} variables;
\item can be expressed as the (a)synchronous composition of other systems.
%%CT redudant
%\item is \emph{hierarchical}, i.e., may include (instances of) previously defined systems as subsystems;
%\item can encode both synchronous and asynchronous system composition.
\end{enumerate}


\paragraph{\bf Atomic systems} 

\moxi defines an \emph{atomic transition system} that has \(m\) inputs, \(n\) outputs, and \(p\) local variables via the command:

\begin{center}
\begin{tabular}{lll}
  & (\texttt{define-system} $S$ & \\
  & ~\texttt{:input} ( (\(i_1\) \(\delta_1\)) \(\cdots\) (\(i_m\) \(\delta_m\)) )
  &  \texttt{:output} ( (\(o_1\) \(\tau_1\)) \(\cdots\) (\(o_n\) \(\tau_n\)) )\\
  & ~\texttt{:local} ( (\(l_1\) \(\sigma_1\)) \(\cdots\) (\(l_p\) \(\sigma_p\)) )
  &  \texttt{:init} \(I\) \texttt{:trans} \(T\) \texttt{:inv} \(P\)), where
\end{tabular}
\end{center}
% \noindent\texttt{(define-system \(S\) ~:input ( (\(i_1\) \(\delta_1\)) \(\cdots\) (\(i_m\) \(\delta_m\)) ) 
% ~:output ( (\(o_1\) \(\tau_1\)) \(\cdots\) (\(o_n\) \(\tau_n\)) ) 
% ~:local ( (\(l_1\) \(\sigma_1\)) \(\cdots\) (\(l_p\) \(\sigma_p\)) )
%  ~:init \(I\) ~:trans \(T\) ~:inv \(P\))}
\vspace{-0.1in}
\begin{itemize}
\item \(S\) is the system's identifier;
\item each \(i_j\) is an \emph{input} variable of sort \(\delta_j\);
\item each \(o_j\) is an \emph{output} variable of sort \(\tau_j\);
\item each \(l_j\) is a \emph{local} variable of sort \(\sigma_j\);
\item each \(i_j\), \(o_j\), \(l_j\) denote \emph{current-state} values;
\item \(I\), \emph{the initial condition}, is a one-state formula over the unprimed system's variables (input, output, and local state variables) that expresses a constraint on the initial states of \(S\);
\item \(T\), \emph{the transition condition,} is a two-state formula over all of the system's variables (primed and unprimed) that expresses a constraint on the state transitions of \(S\);
\item \(P\), \emph{the invariance condition}, is a one-state formula over all of the \emph{unprimed} system's variables that expresses a constraint on all reachable states of \(S\).
\end{itemize}

Next-state variables are not provided explicitly but are denoted by convention by appending \('\) to the names of the current-state variables \(i_j\), \(o_j\), and \(l_j\). Note that all attributes are optional but can occur at most once, and the order of the attributes is immaterial except that \texttt{:input}, \texttt{:output}, and \texttt{:local} must occur before \texttt{:init}, \texttt{:trans}, and \texttt{:inv}. The default value for a missing attribute is the empty list \texttt{()} for \texttt{:input}, \texttt{:output}, and \texttt{:local}; and \texttt{true} for \texttt{:init}, \texttt{:trans}, and \texttt{:inv}.
Syntactically, the system identifier, the input, output, and local variables are  SMT-LIB symbols.
In contrast, the sorts $\delta_j$, $\tau_j$, $\sigma_j$ are SMT-LIB sorts, while the formulas $I$, $T$, and $P$ are SMT-LIB terms of type \texttt{Bool}.

\paragraph{Semantics} Let
$\boldsymbol{i} = (i_1, \ldots, i_m)$,
$\boldsymbol{o} = (o_1, \ldots, o_n)$,
$\boldsymbol{l} = (l_1, \ldots, l_p)$,
and
$\boldsymbol{x}$ = $\boldsymbol{i},\boldsymbol{o},\boldsymbol{l}$.
A system $S$ introduced by the \texttt{define-system} command above is a transition system whose behavior consists of all the (infinite) executions $(\mathcal I, \pi)$ over $\boldsymbol{x}$ such that
$(\mathcal I, \pi) \models I[\boldsymbol{x}] \land \mathbf{always}\ (P[\boldsymbol{x}] \land T[\boldsymbol{x},\boldsymbol{x'}])$.
We call $I_S = I[\boldsymbol{x}]$ \emph{the initial state predicate} of $S$ and
$T_S = P[\boldsymbol{x}] \land T[\boldsymbol{x},\boldsymbol{x'}]$ \emph{the transition predicate} of $S$.


\paragraph{\bf Composite systems}

Transition systems can be defined as the synchronous\footnote{%
The asynchronous composition of systems is planned for a later
version of \moxi.
}
 composition of
other systems using the command:

\begin{center}
\begin{tabular}{l}
  (\texttt{define-system} $S$ 
   \texttt{:input} ( (\(i_1\) \(\delta_1\)) \(\cdots\) (\(i_m\) \(\delta_m\)) )  \\
   \texttt{:output}  ( (\(o_1\) \(\tau_1\)) \(\cdots\) (\( o_n\) \(\tau_n\)) ) 
  \texttt{:local} ( (\(l_1\) \(\sigma_1\)) \(\cdots\) (\(l_p\) \(\sigma_p\)) ) \\
   \texttt{:subsys} (\(N_1\) (\(S_1\) \(\boldsymbol x_1\) \(\boldsymbol y_1\)) )  \(\cdots\) 
  \texttt{:subsys}  (\(N_q\) (\(S_q\) \(\boldsymbol x_q\) \(\boldsymbol y_q\)) ) \\
  \texttt{:init} \(I\) \texttt{:trans} \(T\) \texttt{:inv} \(P\)), where
\end{tabular}
\end{center}
% \noindent\texttt{(define-system \(S\) ~:input ( (\(i_1\) \(\sigma_1\)) \(\cdots\) (\(i_m\) \(\sigma_m\)) ) 
% ~:output ( (\(o_1\) \(\tau_1\)) \(\cdots\) (\(o_n\) \(\tau_n\)) ) 
% ~:local ( (\(l_1\) \(\sigma_1\)) \(\cdots\) (\(l_p\) \(\sigma_p\)) ) 
% ~:subsys (\(N_1\) (\(S_1\) \(\boldsymbol x_1\) \(\boldsymbol y_1\)) ) ~~ \(\cdots\) 
% ~:subsys (\(N_q\) (\(S_q\) \(\boldsymbol x_q\) \(\boldsymbol y_q\)) ) 
% ~:init \(I\) ~:trans \(T\) ~:inv \(P\))}
\vspace{-0.1in}
\begin{itemize}
\item {\tt :input}, {\tt :output}, {\tt:local}, {\tt :init}, {\tt :trans}, and {\tt :inv} are as in atomic system definitions;
\item \(q > 0\) and each \(S_i\) is the name of a system other than \(S\);
\item the names \(S_1 \ldots,S_q\) need not be all distinct;
\item each \(N_i\) is a local synonym for \(S_i\), with \(N_1,\ldots,N_q\) distinct;
\item each \(\boldsymbol x_i\) consists of \(S\)'s variables of the same sort as \(S_i\)'s input;
\item each \(\boldsymbol y_i\) consists of \(S\)'s local/output variables of the same sort as \(S_i\)'s output;
\item the directed subsystem graph rooted at \(S\) is acyclic.
\end{itemize}

\paragraph{Semantics} For $k=1,\ldots, q$, let
$S_k = (I_k[\boldsymbol{i}_k,\boldsymbol{o}_k,\boldsymbol{l}_k], T_k[\boldsymbol{i}_k,\boldsymbol{o}_k,\boldsymbol{l}_k,\boldsymbol{i'}_k,\boldsymbol{o'}_k,\boldsymbol{l'}_k])$,
with the elements of $\boldsymbol{l}_1,\ldots, \boldsymbol{l}_q$ all mutually distinct.
Let
$\boldsymbol{i} = (i_1, \ldots, i_m)$,
$\boldsymbol{o} = (o_1, \ldots, o_n)$,
$\boldsymbol{l} = (l_1, \ldots, l_p), \boldsymbol{l}_1, \ldots, \boldsymbol{l}_q$,
and
$\boldsymbol{x} = \boldsymbol{i}, \boldsymbol{o}, \boldsymbol{l}$.
A composite system $S$ introduced by the \texttt{define-system} command above is a transition system whose behavior consists of all the (infinite) executions
$(\mathcal I, \pi)$ over $\boldsymbol{x}$ such that
$(\mathcal I, \pi) \models
  I_S[\boldsymbol{x}] \land \mathbf{always}\ T_S[\boldsymbol{x},\boldsymbol{x'}]
$, where
%
\begin{itemize}
\item $I_S[\boldsymbol{x}] = I[\boldsymbol{x}] \land \bigwedge_{k=1,\ldots,q} I_k[\boldsymbol{x}_k,\boldsymbol{y}_k,\boldsymbol{l}_k]$ and
\vspace{.2ex}

\item $T_S[\boldsymbol{x},\boldsymbol{x'}] = P[\boldsymbol{x}] \land T[\boldsymbol{x},\boldsymbol{x'}] \land \bigwedge_{k=1,\ldots,q} T_k[\boldsymbol{x}_k,\boldsymbol{y}_k,\boldsymbol{l}_k, \boldsymbol{x'}_k,\boldsymbol{y'}_k,\boldsymbol{l'}_k]$.
\end{itemize}

\subsubsection{Sanity Requirements on $I_S$ and $T_S$}

Every system defined in \moxi is expected to execute forever. 
This is not a limitation in practice because systems meant to reach a final state can be modeled with states that cycle back to themselves and produce stuttering outputs. 
In such semantics, the reachability of a \emph{deadlocked state} (i.e., a state with no successors in the transition relation) indicates the presence of an error in the system's definition. 
For a system definition to define a deadlock-free system, the following must hold for the variables \(\boldsymbol{x} = \boldsymbol{i}, \boldsymbol{o}, \boldsymbol{l}\) and their primed versions.
%\vspace{-0.1in}
\begin{enumerate}[label=(\arabic*)]
\item Every assignment of values to the input variables \(\boldsymbol{i}\) can be extended to an assignment to \(\boldsymbol{x}\) that satisfies \(I_S[\boldsymbol{x}]\).
\item For every reachable state \(s\) (i.e., assignment to the variables \(\boldsymbol{x}\)), every assignment to the primed input variables \(\boldsymbol{i'}\) can be extended to an assignment $s'$ to \(\boldsymbol{x}'\) so that \(s,s'\) satisfies \(T_S[\boldsymbol{x},\boldsymbol{x'}]\).
\end{enumerate}

\noindent
The first restriction guarantees that the system can start.
The second ensures that from any reachable state and for any new input, the system can move to another state (\emph{and} also produce output). Given a specified background theory,
%\vspace{-0.1in}
\begin{itemize}
\item A sufficient condition for (1) is the validity of the formula 
\[\forall \boldsymbol{i}\, \exists \boldsymbol{o}\, \exists \boldsymbol{l}\, I_S[\boldsymbol{i}, \boldsymbol{o}, \boldsymbol{l}]\]

\item A sufficient condition for (2) is the validity of the formula
\[\forall \boldsymbol{i}~ \forall \boldsymbol{o}~ \forall \boldsymbol{l}~
    \forall \boldsymbol{i'}~
    \exists \boldsymbol{o'}~ \exists \boldsymbol{l'}~ T_S[\boldsymbol{i}, \boldsymbol{o}, \boldsymbol{l}, \boldsymbol{i'}, \boldsymbol{o'}, \boldsymbol{l'}]
\]
Note that this is not a necessary condition as it needs not apply to unreachable states. Let \(\textrm{Reachable}[\boldsymbol{i}, \boldsymbol{o}, \boldsymbol{l}]\) denote the (possibly higher-order) formula satisfied exactly by the reachable states of \(S\). 
  Then, a more accurate sufficient condition for (2) above would be the validity of the formula
\[
  \forall \boldsymbol{i}~ \forall \boldsymbol{o}~ \forall \boldsymbol{l}~
  \forall \boldsymbol{i'}~
  \exists \boldsymbol{o'}~ \exists \boldsymbol{l'}~
    \textrm{Reachable}[\boldsymbol{i}, \boldsymbol{o}, \boldsymbol{l}] \Rightarrow T_S[\boldsymbol{i}, \boldsymbol{o}, \boldsymbol{l}, \boldsymbol{i'}, \boldsymbol{o'}, \boldsymbol{l'}]
\]
\end{itemize}

\subsection{System Checking}

%The \texttt{define-system} command defines a (possibly composite) transition system using SMT formulas. 
The properties to check for a (possibly composite) defined system are specified using the following command for defining \emph{queries} on the system's behavior.
%\vspace{-0.1in}
\begin{center}
\begin{tabular}{l}
  (\texttt{check-system} $S$ \\
  ~\texttt{:input} ( (\(i_1\) \(\delta_1\)) \(\cdots\) (\(i_m\) \(\delta_m\)) ) 
   \texttt{:output}  ( (\(o_1\) \(\tau_1\)) \(\cdots\) (\(o_n\) \(\tau_n\)) ) \\
  ~\texttt{:local} ( (\(l_1\) \(\sigma_1\)) \(\cdots\) (\(l_p\) \(\sigma_p\)) )
   \texttt{:assumption} (\(a\) A ) \texttt{:fairness} (\(f\) \(F\))  \\
  ~\texttt{:reachable} (\(r\) \(R\)) \texttt{:current} (\(c\) \(C\)) 
  ~\texttt{:query}  (\(q\) (\(g_1\) \(\cdots\) \(g_q\)) )  \\
   \texttt{:queries} ( (\(q_1\) (\(g_{1,1}\) \(\cdots\) \(g_{1,n_1}\)) ) \(\cdots\) (\(q_t\) (\(g_{t,1}\) \(\cdots\) \(g_{t,n_t}\)) ) )), where
\end{tabular}
\end{center}
\vspace{-0.1in}
\begin{itemize}
\item \(S\) is the identifier of a system with \(m\) inputs, \(n\) outputs, and \(p\) local variables;

% \item all attributes are optional and their order is immaterial except that :input, :output, :local, have to come before the other attributes {[}may not need this restriction{]};
% \item all attributes except for :input, :output and :local are repeatable.

\item \(\boldsymbol{i} = (i_1, \ldots, i_m)\) is a renaming of input variables in \(S\) of sort \(\boldsymbol{\delta} = (\delta_1, \ldots, \delta_m)\);

\item \(\boldsymbol{o} = (o_1, \ldots, o_n)\) is a renaming of output variables in \(S\) of sort \(\boldsymbol{\tau} = (\tau_1, \ldots, \tau_n)\);

\item \(\boldsymbol{l} = (l_1, \ldots, l_p)\) is a renaming of local variables in \(S\) of sort \(\boldsymbol{\sigma} = (\sigma_1, \ldots, \sigma_p)\);
\item
  \(a\), \(r\), \(f\), \(c\), \(q\), \(q_1, \ldots, q_k\) are
  identifiers;
\item
  \(A\) is a formula over \(\boldsymbol{i}\), \(\boldsymbol{o}\), \(\boldsymbol{l}\), \(\boldsymbol{i'}\) expressing an \emph{assumption} on
  \(\boldsymbol{i'}\);
\item
  \(F\) is a formula over \(\boldsymbol{i}\), \(\boldsymbol{o}\), \(\boldsymbol{l}\),
  \(\boldsymbol{i'}\) expressing a \emph{fairness condition} on
  \(\boldsymbol{i'}\);
\item
  \(R\) is a formula over  \(\boldsymbol{i}\), \(\boldsymbol{o}\), \(\boldsymbol{l}\),  \(\boldsymbol{i'}\), \(\boldsymbol{o'}\), \(\boldsymbol{l'}\) expressing a state \emph{reachability condition};
\item
  \(C\) is a formula over  \(\boldsymbol{i}\), \(\boldsymbol{o}\), \(\boldsymbol{l}\)
  expressing a state \emph{initiality condition};
\item
  each \(g_j\) and \(g_{j,k}\) ranges over the \(a\), \(r\), \(f\),
  \(c\) identifiers;
\item
  \((q\ (g_1 \cdots g_q))\) defines a query \(q\) as consisting of the
  formulas named by \(g_1, \dots, g_q\); the same holds for each
  \((q_j\ (g_{j,1} \cdots g_{j,n_j}))\).
\end{itemize}

Note that $A$, $F$, $R$, and $C$ are all non-temporal formulas. 
Each of the attributes \texttt{:assumption}, \texttt{:reachable}, \texttt{:query}, and \texttt{:queries} can occur zero or more times.
Moreover, a query can contain more than one assumption, fairness condition, and reachability condition but at most one initiality condition.

\paragraph{Semantics} Each query (\(q\) and each \(q_j\)) in the \texttt{check-system} command asks for the existence of a trace. 
The query is to be evaluated with infinite-state semantics if it includes at least one fairness condition, and finite-state semantics otherwise.
Specifically, for a system \(S\), let \(I_S\) and \(T_S\) be the initial state and transition predicates of \(S\) \emph{modulo} the variable renamings in the \texttt{check-system} command. Let \(t, u, v  \geq 0\). The semantics of a query are defined as follows:

\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\item A query of the form (\(a_1\) \(\cdots\) \(a_t\) \(r_1\)
  \(\cdots\) \(r_u\)), where each \(a_j\) and \(r_j\) identify an assumption \(A_j\) and reachability condition \(R_j\), respectively, is \emph{satisfiable} iff

\begin{center}
\begin{tabular}{rcl}
  $I_S$ & $\land$ & $\mathbf{always}\ T_S$ \\
  & $\land$ & $\mathbf{always}\ (A_1 \land \cdots \land A_t)$ \\
  & $\land$ & $\mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u$
\end{tabular}
\end{center}

is \textbf{\(n\)-satisfiable} in LTL for some \(n \geq 0\).
\end{enumerate}
\vspace{-0.1in}
\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\setcounter{enumi}{1}
\item
  A query of the form (\(c\) \(a_1\) \(\cdots\) \(a_t\) \(r_1\) \(\cdots\) \(r_u\)), where \(c\) is the initiality condition \(C\), and each \(a_j\) and \(r_j\) identify an assumption \(A_j\) and reachability condition \(R_j\), respectively, is \emph{satisfiable} iff

\begin{center}
\begin{tabular}{rcl}
  $C$ & $\land$ & $\mathbf{always}\ T_S$ \\
  & $\land$ & $\mathbf{always}\ (A_1 \land \cdots \land A_t)$ \\
  & $\land$ & $\mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u$
\end{tabular}
\end{center}

is \textbf{\(n\)-satisfiable} in LTL for some \(n \geq 0\).
\end{enumerate}
\vspace{-0.1in}
\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\setcounter{enumi}{2}
\item
  A query of the form (\(a_1\) \(\cdots\) \(a_t\) \(r_1\)
  \(\cdots\) \(r_u\) \(f_1\) \(\cdots\) \(f_v\)), where each \(a_j\), \(r_j\), and \(f_j\) identify an assumption \(A_j\), a reachability
  condition \(R_j\), and a fairness condition \(F_j\), respectively, is \emph{satisfiable} iff

\begin{center}
\begin{tabular}{rcl}
   $I_S$
   & $\land$ & $\mathbf{always}\ T_S$ \\
   & $\land$ & $\mathbf{always}\ (A_1 \land \cdots \land A_t)$ \\
   & $\land$ & $\mathbf{always}\ \mathbf{eventually}\ F_1 \land \cdots
 \land   \mathbf{always}\ \mathbf{eventually}\ F_v$ \\
   & $\land$ & $\mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u$
\end{tabular}
\end{center}

is \textbf{satisfiable} in LTL.
\end{enumerate}

\vspace{-0.1in}
\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\setcounter{enumi}{3}
\item
  A query of the form (\(c\) \(a_1\) \(\cdots\) \(a_t\) \(r_1\) \(\cdots\) \(r_u\) \(f_1\) \(\cdots\) \(f_v\)),  where \(c\) is the initiality condition \(C\) and each \(a_j\), \(r_j\), and \(f_j\) identify an assumption \(A_j\), a reachability condition \(R_j\), and a fairness condition \(F_j\), respectively, is \emph{satisfiable} iff 

\begin{center}
\begin{tabular}{rcl}
   $C$
   & $\land$ & $\mathbf{always}\ T_S$ \\
   & $\land$ & $\mathbf{always}\ (A_1 \land \cdots \land A_t)$ \\
   & $\land$ & $\mathbf{always}\ \mathbf{eventually}\ F_1 \land \cdots
 \land   \mathbf{always}\ \mathbf{eventually}\ F_v$ \\
   & $\land$ & $\mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u$
\end{tabular}
\end{center}
is \textbf{satisfiable} in LTL.
\end{enumerate}

\noindent
Let \(\mathcal T\) be the background theory specified for a \moxi
model. For each satisfiable query in the \texttt{check-system} command, the back-end model checking algorithm is expected to produce
\begin{enumerate*}[label={(\arabic*)}]
\item
  a \(\mathcal T\)-interpretation \(\mathcal I\) of the (global) free symbols in the script;
\item a witnessing trace in \(\mathcal I\).
\end{enumerate*}
For each unsatisfiable query, the model checker may return 
a \emph{proof certificate} for that query's unsatisfiability.

The interpretation \(\mathcal I\) \emph{must be the same} for all queries in the same \texttt{:queries} attribute. In
contrast, queries in different attributes may each interpret the free symbols differently. Regardless of where it
occurs, each query may have its own witnessing trace.

\subsection{System Checking Response}

\moxi also defines the content and format of possible responses (from the back-end model checker) to a \texttt{check-system} command. Witness traces returned by the model checker are currently limited to \emph{lasso} traces, that is, traces of the form $pl^\omega$, where $p$ and $l$ are finite sequences of state, or \emph{trails}.
Each witness is then represented by two trails: \begin{enumerate*}[label=(\arabic*)] \item a \emph{prefix trail} $p$, and \item a \emph{lasso trail} $l$.\end{enumerate*} 
In contrast, a proof certificate for a trace represents a proof 
of the unsatisfiability of the query.
Currently, \moxi does not specify the format of proof certificates
except for requiring them to be SMT-LIB S-expressions.
Figure~\ref{fig:response} shows the format 
for a \texttt{check-system} command with
input \texttt{i}, 
output \texttt{o},
local variable \texttt{s}, and
queries \texttt{q1}, \texttt{q2}, \texttt{q3}, 
where \texttt{q1} has 
a reachability condition \texttt{r} and
fairness condition \texttt{f}.

\begin{figure}[t]
\begin{lstlisting}[language=MoXI]
(check-system-response
 :verbosity full
 :query (q1 :result sat :model m :trace t)
 :query (q2 :result unsat :certificate c)
 :query (q3 :result unknown)   ; for timeouts and other cases
 :trace (t :prefix p :lasso l) ; t = pl^w
 :model (m M)                  ; M is an interpr. in SMT-LIB format
 :trail (p ((0 (i i0) (o o0) (s s0) (r r0) (f f0)); first state in p
             ...
            (j (i ij) (o oj) (s sj) (r rj) (f fj)); last state in p
           )
        ) 
 :trail (l ( ( ... ) ... ( ... ) )) ; similar to p
 :certificate (c ... )
)
\end{lstlisting}
\caption{Format of a model checker's response to a \texttt{check-system} command.}
\label{fig:response}
\medskip
\end{figure}



\subsection{Example} \label{sec:example}

As an illustrative example of a \moxi model, consider a timed switch with a single Boolean input and output where the output \emph{switches} from its current value if the next input is true or the output has been true for at least 10 consecutive steps. 
Figure~\ref{fig:switch} shows a full definition of such a system in \moxi.


\begin{figure}[h]
\begin{lstlisting}[language=MoXI]
  (set-logic QF_LIA)
  (declare-enum-sort LightStatus (on off))

  (define-system TimedSwitch :input ( (press Bool) )
   :output ( (sig Bool) )
   :local ( (s LightStatus) (n Int) )
   :inv (= sig (= s on))
   :init (and (= n 0) (= s (ite press on off)))
   :trans (let (; transitions
      (turn-on  (and (= s off) press' (= s' on) (= n' n)))
      (stay-on  (and (= s on) (< n 10) (not press') 
                     (= s' on) (= n' (+ n 1))))
      (turn-off (and (= s on) (or (>= n 10) press') 
                     (= s' off) (= n' 0)))
      (stay-off (and (= s off) (not press') (= s' off) (= n' n)))
     )
     (or turn-on stay-on turn-off stay-off)
   )
  )

  (check-system TimedSwitch :input ( (press Bool) ) 
   :output ( (sig Bool) )
   :local ( (s LightStatus) (n Int) )
   :reachable (r1 (and press (not sig) (= s off)))
   :query (q1 (r1))
  )
\end{lstlisting}
%\vspace{-0.1in}
\caption{Example \moxi model of a timed switch with a 10-step timeout.}
\label{fig:switch}
\medskip
\end{figure}

To start, we select the SMT-LIB logic \texttt{QF-LIA}, which restricts the language of formulas to quantifier-free formulas over linear integer arithmetic.
Then, we declare an enumeration sort to represent the internal state of the switch.
Next, we define the timed switch itself.
This begins by declaring its input variable \texttt{press}, output variable \texttt{sig}, and local variables \texttt{s} and \texttt{n} to track,
respectively, the switch's current state (on or off) and the number of steps the switch has been continuously set to \texttt{on}.
In the same definition, on line 8, we define an invariant stating that \texttt{sig} is true exactly when the value of \texttt{s} is \texttt{on}.
The initial condition, on line 9, sets \texttt{n} to 0 and \texttt{s} 
to the enumeration value corresponding to the initial value of \texttt{press}. 
We finish up the definition of \texttt{TimedSwitch} with the transition relation on lines 9-19, provided in \emph{named transition} style,\footnote{%
\moxi's syntax also supports other styles, such as equational or condition-action.
}
where we define each possible transition separately and one of the transitions gets non-deterministically chosen each time. In our case, we have four possibilities based on the pre- and post-state of the transition as follows.
\begin{description}
  \item[\texttt{turn-on}:] when \texttt{s} is off in the pre-state and \texttt{press} is true in the post-state.
  \item[\texttt{stay-on}:] when \texttt{s} is on and \texttt{n} $< 10$ in the pre-state, and \texttt{press} is false in the post-state.
  \item[\texttt{turn-off:}] when \texttt{s} is on in the pre-state and either \texttt{n} is at least 10 in the pre-state or \texttt{press} is false in the post-state.
  \item[\texttt{stay-off}:] when \texttt{s} is off in the pre-state and \texttt{press} is false in the post-state.
\end{description}
Finally, on lines 21-26, we issue a check request on the system, asking whether it can reach a state where \texttt{press} is true, \texttt{sig} is false, and \texttt{s} is off. Figure~\ref{fig:switchres} provides a possible response to this request. It shows a finite trace, represented as a lasso trace with an empty lasso, where the transition \texttt{turn-off} is taken immediately from an initial state (state $0$) where \texttt{s} is on.

\begin{figure}[t]
\begin{lstlisting}[language=MoXI]
(check-system-response TimedSwitch
  :query (q1 :result sat :trace w1)
  :trace (w1 :prefix t1)
  :trail (t1 (0 (n 0) (s on) (sig true) (press true))
             (1 (n 0) (s off) (sig false) (press true)))
)
\end{lstlisting}
\caption{A possible response to the \texttt{check-system} command from Figure~\ref{fig:switch}.}
\label{fig:switchres}
\end{figure}


% \vspace{-0.1in}
% \subsection{Formal Semantics}\label{sec:}
% \vspace{-0.1in}

% \vspace{-0.1in}
% \subsection{Proofs}\label{sec:}
% \vspace{-0.1in}

% Thereom: There is a MoXI structure whose language is exactly L(f) for any LTl formula f.
% Proof: KYR can write. Probably proof goes in appendix.

% What other theorems do we have?


%\vspace{-0.1in}
\section{Translator Toolchain}\label{sec:translator}
%\vspace{-0.1in}

A core application for \moxi is as an intermediate language in a toolchain integrating a high-level modeling language and a low-level representation for a model-checking back end. As Figure~\ref{fig:toolchain} shows, this allows users to write models in an intuitive, high-level language while also leveraging state-of-the-art algorithms provided by model checkers that accept a low-level language as input.

\begin{figure}
  \centering
  \includegraphics[width=\textwidth]{img/abstract_toolchain.png}
  \vspace{0.02in}
  \caption{The abstract translator toolchain provides translators from a high-level model to low-level model via \moxi, and back for generated witnesses. Blue denotes models and their queries, green denotes a translator, and yellow denotes a witness. Examples of high-level languages include SMV and Verilog; low-level languages include \btor and \aiger. All blue boxes are behaviorally equivalent, as are all yellow boxes.}
  \label{fig:toolchain}
\end{figure}

%\vspace{-0.1in}
\subsubsection{Prototype Implementation}
%
We provide a prototype Python implementation of such a toolchain, using SMV and \btor as the high-level and low-level languages, respectively~\cite{JNDISTVR24}. We selected SMV due to its ubiquity in modeling symbolic transition systems~\cite{RLS02,GHBTCM02,TM03,CH03,MTWH06,Mil08,YJC09,BCKNNR09,GDH11,LVBFNH12,BCFJKPRT15,ZR12,ZR14,MCGTR15,GCMTR16,DRR17,DR17} and \btor due to it being the input language for the most-recent 2020 Hardware Model Checking Competition~\cite{hwmcc20}.
%
The toolchain translates SMV models to behaviorally equivalent \moxi models, and subsequently to \btor models. Then, the tool translates responses from a \btor model checker back to SMV-style responses via \moxi responses. 

% Chris: Do we cite the CAV tool paper under submission?

%\vspace{-0.1in}
\subsubsection{Experimental Evaluation}
%
To evaluate the effectiveness of our toolchain, we ran it over the set of 960 \texttt{QF\_BV} and \texttt{QF\_ABV} benchmarks provided with the \nuXmv public release and compared the performance of a variety of back-end model checkers: \avr~\cite{GS20} (\texttt{hwmcc20} GitHub branch), \nuXmv~\cite{CCDGMMMRT2014} (\texttt{version 2.0} --- latest public release), and \pono~\cite{MILYZBGB21} (\texttt{commit \#b243cef} --- latest development head). 

We ran two experiments: the first ran each solver using IC3-based~\cite{Bra11} algorithms and the second ran each solver using a portfolio approach of BMC, K-Induction, and IC3-based algorithms. In the latter case, we collected the best time among the three techniques.
For each experiment, we ran \nuXmv directly on the SMV benchmarks, i.e., SMV $\rightarrow$ \nuXmv, and ran the other two solvers on \btor generated from the toolchain presented above, i.e., SMV $\rightarrow$ \moxi $\rightarrow$ \btor $\rightarrow$ \avr/\pono and back. 
Here are some details about each tool.   %\vspace{-0.1in}
\begin{itemize}
  \item \avr (Yices2~\cite{Yices} as the back-end SMT solver): BMC~\cite{biere99satmc}, K-induction based on~\cite{SSS00}, IC3 based on~\cite{goel2019model}.
  \item \nuXmv (MathSAT5~\cite{CGSS13} as the back-end SMT solver): BMC~\cite{biere99satmc}, K-induction based on~\cite{een2003temporal}, and IC3 based on~\cite{cimatti2014ic3}.
  \item \pono (Boolector~\cite{NPWB2018} and MathSAT5~\cite{CGSS13} as back-end SMT solvers): BMC~\cite{biere99satmc}, K-induction based on~\cite{een2003temporal}, IC3 based on~\cite{cimatti2014ic3}.
\end{itemize}

\begin{figure}[t]
  \centering
  \begin{tikzpicture}
    \begin{axis}[
        width=\textwidth,
        height=2in,
        xmin=-200, xmax=3600,
        % xlabel={Wall-clock Time (s)},
        ylabel={\# Solved},
        xticklabel=\empty,
        legend style={nodes={scale=0.7, transform shape}},
        legend entries={\avr-ic3,\pono-ic3,\nuXmv-ic3,vb-ic3},
        legend pos=south east,
        legend columns=2,
    ]
    
    \addplot[color=blue, mark=x] table {data/avr-ic3.dat};
    \addplot[color=orange, mark=square] table {data/pono-ic3.dat};
    \addplot[color=bluegreen, mark=triangle] table {data/nuxmv-ic3.dat};
    \addplot[color=purple, mark=o, style=thick] table {data/vb-ic3.dat};
        
    \end{axis}
  \end{tikzpicture} \\
  \begin{tikzpicture}
    \begin{axis}[
        width=\textwidth,
        height=2in,
        xmin=-200, xmax=3600,
        % ymin=-30, ymax=160,
        xlabel={Wall-clock Time (s)},
        ylabel={\# Solved},
        legend style={nodes={scale=0.7, transform shape}},
        legend entries={
          vb-\avr,
          vb-\pono,
          % vb-\btormc,
          vb-\nuXmv,
          vb-all
        },
        legend pos=south east,
        legend columns=2,
    ]
    
    \addplot[color=blue, mark=x] table {data/vb-avr.dat};
    \addplot[color=orange, mark=square] table {data/vb-pono.dat};
    % \addplot[color=red, mark=Mercedes star] table {data/vb-btormc.dat};
    \addplot[color=bluegreen, mark=triangle] table {data/vb-nuxmv.dat};
    \addplot[color=purple, mark=o, style=thick] table {data/vb-all.dat};
    \end{axis}
  \end{tikzpicture}
  \caption{
   Performance comparison on SMV-language benchmark queries using IC3 (Top) and portfolio approach (Bottom) across three different model checkers: SMV benchmarks $\rightarrow$ \nuXmv, a translation of SMV benchmarks $\rightarrow$ \moxi $\rightarrow$ \btor $\rightarrow$ \avr (and back), and a translation of SMV benchmarks $\rightarrow$ \moxi $\rightarrow$ \btor $\rightarrow$ \pono (and back). The vb-* represents the virtual-best back-end solver for each model checker. The portfolio approach represents the best time using BMC, k-induction, and IC3 algorithms. Wall-clock time for the non-\nuXmv plots include translation time.
  }
  \label{fig:cactus}
\end{figure}

\noindent
In all cases, no discrepancies were found, i.e., no two model checkers returned conflicting \emph{safe} and \emph{unsafe} results, and all generated \btor was well-formed according to the reference checker \catbtor~\cite{NPWB2018}.

% discuss results
As the top of Figure~\ref{fig:cactus} shows, the three model checkers \nuXmv, \avr, and \pono complement each other when using their IC3-based algorithms; each solver performs similarly, but the virtual-best outperforms each individual by a noticeable margin.
Similarly, the bottom of Figure~\ref{fig:cactus} shows that while the model checkers perform similarly using a portfolio approach, they again complement each other, as shown by the virtual-best outperforming each model checker individually. Importantly, our initial, non-optimized translation of SMV-language benchmarks through \moxi does not inhibit the model checking performance of either \avr or \pono, compared to using \nuXmv directly on the same SMV-language benchmarks distributed with that tool. 

%\vspace{-0.1in}

\section{Future Directions for Symbolic Model Checking}\label{sec:discussion}
%\vspace{-0.1in}

Creating an international standard for symbolic model checking changes the landscape of research next steps, from low-hanging fruit to future challenges. There is even more reason to continue and expand on current research directions aimed at breaking down the barriers to the wider adoption of symbolic model checking by addressing (1) the specification bottleneck; and (2) the state-space explosion problem. Having laid a foundation for standardization, we hope that the community can converge on \moxi as a common intermediate language and leverage this standard in pursing research directions that make advances in areas (1) and (2).

\paragraph{High-level language translation.} In addition to creating translations for existing high-level modeling languages to/from \moxi, there is now an opportunity to create new languages that take advantage of the access to back-end algorithms that \moxi provides. Current model-checking high-level languages were designed to be as general as possible, to represent a reasonably broad class of systems since usually each model-checking tool accepts only one modeling language. Now, there is more room for highly-specialized, system-specific languages, further mitigating the specification bottleneck.

\paragraph{Low-level language translation.} To loop in current and future model-checking back-end algorithms, we need translations between \moxi and the low-level representations used by model-checking tools. Future algorithms may be designed with such a translation in mind. Though it was designed as an intermediate language, \moxi may be sufficiently low-level to serve as the input representation for future back-end tools; this is another avenue worth investigating. 

\paragraph{Translation optimizations.} We provide initial translations between the high-level SMV language and \moxi, and between \moxi and the low-level representation \btor\cite{JNDISTVR24}. However, these are just proofs of concept. They demonstrate that a translation is possible and that the design of \moxi maintains the expressiveness we intended. These translations were not designed to be optimal, or even efficient, only correct and, hopefully, transparent. Our initial toolchain encodes LTL specifications by using PANDA \cite{RV11} to translate them into SMV, then translating the PANDA-generated SMV models to \moxi; exploring direct LTL-to-\moxi translations could improve model-checking performance. Section \ref{sec:translator} demonstrates that model checking through \moxi does not exacerbate the state-space explosion problem, but there is certainly ample room for improvement. We expect a progression of future papers creating increasingly performant translations, improving upon our translations and those contributed by others (see above). 

\paragraph{Proofs and benchmarks.} While we have extensively investigated the correctness of our initial \moxi translations, we have yet to prove them correct formally, for instance by using an interactive theorem prover. We believe it is possible, though challenging, to state the semantic equivalence of representations in a high- or low-level language and \moxi as theorems, prove them correct using a theorem prover like PVS, and then generate verified translators using a tool like PVS2C \cite{DBLP:conf/vmcai/CourantSS20,Ferey2016}.\footnote{Thanks to Laura Gamboa Guzman, Katherine Kosaian, and Yi Lin for their initial investigations into this possibility.} Lower-hanging fruit involves creating, packaging, and releasing benchmarks for \moxi translations that help others check their new translations and serve as performance checkpoints for translation tools.

\paragraph{Extensions. } Though we have initially addressed hardware model checking of finite-state systems, \moxi is extensible by design. Future research directions include further extending \moxi representations to infinite-state model checking, investigating efficient representations for highly-expressive high-level modeling languages, and even exploring the uses of \moxi for applications in software model checking.\footnote{Thanks to Dirk Beyer for initial ideas in this direction.}


\bibliographystyle{splncs04}
\bibliography{../consolidated.bib}
% \input{tex/appendix}

\end{document}
