Related papers: Formal Verification of Self-Assembling Systems
The increasing use of model-based tools enables further use of formal verification techniques in the context of distributed real-time systems. To avoid state explosion, it is necessary to construct verification models that focus on the…
In this paper, we investigate shape-assembling power of a tile-based model of self-assembly called the Signal-Passing Tile Assembly Model (STAM). In this model, the glues that bind tiles together can be turned on and off by the binding…
Model checking and automated theorem proving are two pillars of formal methods. This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and…
In the self-assembly process which drives the formation of cellular membranes, micelles, and capsids, a collection of separated subunits spontaneously binds together to form functional and more ordered structures. In this work, we study the…
This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational (i.e., automata-based) and descriptive (i.e., logic-based)…
We introduce a new model of algorithmic tile self-assembly called size-dependent assembly. In previous models, supertiles are stable when the total strength of the bonds between any two halves exceeds some constant temperature. In this…
In this paper we investigate the computational power of the polygonal tile assembly model (polygonal TAM) at temperature 1, i.e. in non-cooperative systems. The polygonal TAM is an extension of Winfree's abstract tile assembly model (aTAM)…
In this paper, we investigate the abilities of systems of self-assembling tiles which can each pass a constant number of signals to their immediate neighbors to create replicas of input shapes. Namely, we work within the Signal-passing Tile…
Recent studies have demonstrated that test-time compute scaling effectively improves the performance of small language models (sLMs). However, prior research has mainly examined test-time compute scaling with an additional larger model as a…
Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task that is notoriously…
Diffusion Multi-modal Large Language Models (dMLLMs) have recently emerged as a novel architecture unifying image generation and understanding. However, developing effective and efficient Test-Time Scaling (TTS) methods to unlock their full…
Large language models (LLMs) have demonstrated significant potential in formal theorem proving, yet state-of-the-art performance often necessitates prohibitive test-time compute via massive roll-outs or extended context windows. In this…
We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL+ of the full Alternating time temporal logic ATL*. The method extends…
Temporal logic is a very powerful formalism deeply investigated and used in formal system design and verification. Its application usually reduces to solving specific decision problems such as model checking and satisfiability. In these…
Recently there has been a great attention from the scientific community towards the use of the model-checking technique as a tool for test generation in the simulation field. This paper aims to provide a useful mean to get more insights…
I consider the following generic scenario: an abstract model M of some 'real' system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in some…
DNA Self-Assembly has emerged as an interdisciplinary field with many intriguing applications such DNA bio-sensor, DNA circuits, DNA storage, drug delivery etc. Tile assembly model of DNA has been studied for various computational…
Self-assembly is ubiquitous in nature, particularly in biology, where it underlies the formation of protein quaternary structure and protein aggregation. Quaternary structure assembles deterministically and performs a wide range of…
We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a desired temporal logic…
The Tile Automata (TA) model describes self-assembly systems in which monomers can build structures and transition with an adjacent monomer to change their states. This paper shows that seeded TA is a non-committal intrinsically universal…