Client-server systems are a computing paradigm in concurrent and distributed systems. We deal with unbounded client-server systems (UCS) where all clients are of the same type, interact with a single server and they may enter and exit the system dynamically. At any point in time, the number of clients is bounded, but their exact number is unknown and dynamic. To model these systems, simple Petri nets are not directly usable, so we use unbounded $ν$-nets. Owing to the distinguishability of clients in UCS, it is not straightforward to express their properties in LTL or CTL. To address this, we propose the logic $\mathsf{FOTL_1}$, a monodic fragment of Monadic First Order Temporal Logic (MFOTL). In this work, we provide the SMT encodings of $ν$-nets and $\mathsf{FOTL_1}$ to do Bounded Model Checking (BMC). We also build an accompanying open source tool to perform BMC of UCS.

翻译：客户端-服务器系统是并发与分布式系统中的一种计算范式。本文研究所有客户端属于同一类型、与单一服务器交互且可动态进出系统的无界客户端-服务器系统。在任何时刻，客户端数量均存在上界，但其具体数量未知且动态变化。由于简单Petri网无法直接对此类系统建模，我们采用无界$ν$-网进行形式化描述。鉴于UCS中客户端的可区分特性，其性质难以直接用LTL或CTL表达。为此，我们提出$\mathsf{FOTL_1}$逻辑——一种单子一阶时序逻辑的单元片段。本研究通过构建$ν$-网与$\mathsf{FOTL_1}$的SMT编码实现有界模型检测，并开发了配套开源工具以支持UCS的BMC验证。