Paper
Verification of Unbounded Client-Server Systems with Distinguishable Clients
Authors
Ramchandra Phawade, Tephilla Prince, S Sheerazuddin
Abstract
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.
Metadata
Related papers
Fractal universe and quantum gravity made simple
Fabio Briscese, Gianluca Calcagni • 2026-03-25
POLY-SIM: Polyglot Speaker Identification with Missing Modality Grand Challenge 2026 Evaluation Plan
Marta Moscati, Muhammad Saad Saeed, Marina Zanoni, Mubashir Noman, Rohan Kuma... • 2026-03-25
LensWalk: Agentic Video Understanding by Planning How You See in Videos
Keliang Li, Yansong Li, Hongze Shen, Mengdi Liu, Hong Chang, Shiguang Shan • 2026-03-25
Orientation Reconstruction of Proteins using Coulomb Explosions
Tomas André, Alfredo Bellisario, Nicusor Timneanu, Carl Caleman • 2026-03-25
The role of spatial context and multitask learning in the detection of organic and conventional farming systems based on Sentinel-2 time series
Jan Hemmerling, Marcel Schwieder, Philippe Rufin, Leon-Friedrich Thomas, Mire... • 2026-03-25
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2602.23054v1</id>\n <title>Verification of Unbounded Client-Server Systems with Distinguishable Clients</title>\n <updated>2026-02-26T14:40:22Z</updated>\n <link href='https://arxiv.org/abs/2602.23054v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2602.23054v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>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.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.LO'/>\n <published>2026-02-26T14:40:22Z</published>\n <arxiv:primary_category term='cs.LO'/>\n <author>\n <name>Ramchandra Phawade</name>\n </author>\n <author>\n <name>Tephilla Prince</name>\n </author>\n <author>\n <name>S Sheerazuddin</name>\n </author>\n </entry>"
}