Late Weak Bisimulation for Markov Automata
弱双相似性是马尔可夫自动机的一个基于分布的等价概念。它作为马尔可夫自动机上的粗略合理的行为等价已经得到了一些普及。本文研究了一个严格粗糙的概念:晚弱双相似性享有有价值的属性,如果限制到重要的子类的标记:迹分布等价隐含的部分信息标记,和组合性保持分布式标记。因此,两个调度程序类的交集跨越了马尔可夫自动机的一个更粗糙但仍然合理的组合理论。
2014-01-14 cs.FL
Weak Cost Register Automata are Still Powerful
我们考虑一个最弱的变种的成本寄存器自动机在热带半环,即无拷贝成本寄存器自动机在$\mathbb{N}$更新使用$\min$和增量。我们表明,该模型可以模拟,在某种意义上,运行计数器机与零测试。我们推断出与该模型相关的一些问题是不可判定的,特别是等价性,从而反驳了2012年的一个猜想。为了强调这些机器有多弱,我们还证明了它们可以表示为线性模糊加权自动机的限制形式。
2018-04-17 cs.FL
Weak and Nested Class Memory Automata
无限字母表上的自动机作为解决验证和数据库理论问题的潜在有用工具,最近得到了广泛的研究。一个流行的模型研究的自动机是类记忆自动机(CMA),其中的空性问题相当于Petri网的可达性。我们确定了一个限制-我们称之为弱点-CMA,并表明其空性问题是等价于Petri网的覆盖性。此外,我们表明,在确定性的情况下,他们是封闭的所有布尔运算。我们澄清弱CMA和现有的自动机之间的连接数据语言。我们还扩展CMA操作多层次的嵌套数据值,并表明,虽然这些具有不可判定的空虚一般,增加弱点约束恢复可判定性的空虚,通过减少覆盖良好结构的过渡系统。我们还研究了嵌套数据与现有自动机的连接。
2014-11-28 cs.FL
Regular Monoidal Languages
我们介绍了自由monoidal范畴中态射的正则语言,以及它们的相关文法和自动机。这些方法颠覆了关于词和树的正则语言的经典理论,而且还在字符串图上开辟了更广泛的语言类别。利用Monoidal和Carnival限制范畴的代数来研究正则Monoidal语言的性质,并给出了确定Monoidal自动机可识别正则Monoidal语言的充分条件.
2022-07-01 cs.FL math.CT
A Quasi-Linear Time Algorithm Deciding Whether Weak Büchi Automata Reading Vectors of Reals Recognize Saturated Languages
这项工作考虑弱确定性Büchi自动机阅读编码的非负$d$ -向量的实数在一个固定的基地。饱和语言是一种语言,它包含属于实数的一组$d$ -向量的元素的所有编码。实向量自动机是一种识别饱和语言的自动机。说明了如何在拟线性时间内判定一个极小弱确定Büchi自动机是否为实向量自动机。这个问题解决了两个标准的编码向量的数字:顺序编码和并行编码。对于接受实数集的最小弱Büchi自动机,该算法在线性时间内运行。最后,还解决了自动机读取相对实数向量的并行编码问题。
2017-03-14 cs.FL
Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time
在概率自动机的背景下,以有效的方式确定弱概率互模拟是一个开放的问题,大约十年。在这项工作中,我们关闭这个问题,提出了一个程序,在多项式时间检查存在一个弱的组合过渡满足步骤条件的互模拟。我们还提出了几个弱组合转移的扩展,如超转移和新的概念,允许弱组合和超转移和等价匹配,原来是可验证的多项式时间以及。这些结果为概率系统更有效的成分分析算法的发展奠定了基础。
2012-07-15 cs.FL
Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata
本文提出一种将交替弱Büchi自动机(AWA)翻译为无歧义Büchi自动机(UBA)的方法,实现了单指数级膨胀,并直接提供了LDL到UBA的单指数翻译,且复杂度低于已知最佳的NBA去歧义算法。
2023-05-17 cs.FL
On Semantically-Deterministic Automata
本文研究无限词上的语义确定性自动机,证明SD Büchi和co-Büchi自动机比确定性自动机指数级更简洁但补运算和决策问题更难,而SD weak自动机可高效确定化。
2023-05-24 cs.FL
Efficient Learning of Weak Deterministic Büchi Automata
针对弱确定性Büchi自动机(wDBAs),提出高效Angluin风格学习算法,利用其最小范式特性,将查询数量从五次多项式降至规范wDBA大小的二次多项式,理论优势在基准测试中得到验证。
2025-08-19 cs.FL
Feasible Automata for Two-Variable Logic with Successor on Data Words
我们介绍了一个自动机模型的数据字,这是在每个位置进行一个符号从一个有限的字母表和一个值从一个无界的数据域的话。该模型是(语义)的数据自动机,介绍了Bojanczyk,等的限制。在2006年,它被称为弱数据自动机。它的表达能力比数据自动机差,而表达能力又是寄存器自动机无法比拟的。弱数据自动机的表达能力与后继为+1且数据值相等\sim,EMSO 2(+1,\sim)的存在一元二阶逻辑完全对应。它遵循从以前的工作,大卫,等。等人在2010年提出了弱数据自动机的非空性问题可以在2-NEXPTIME中判定。此外,我们还研究了数据ω-串上的弱Büchi自动机。它们可以用EMSO 2(+1,\sim)的扩展来刻画,其中存在量词用于无限集合.最后,通过对弱数据自动机的非空性问题进行非确定性多项式时间约简,得到了其非空性问题的复杂性界。
2011-10-06 cs.FL cs.LO
Markov Automata: Deciding Weak Bisimulation by means of non-naively Vanishing States
提出了一种基于马尔可夫自动机的弱互模拟判定算法。为此,定义了消失状态的不同概念(从广义随机Petri网领域已知的概念)。消失状态是必不可少的相关概念(基于状态)天真的弱互模拟和(基于分布)弱互模拟。本文提出的互模拟算法遵循划分-细化方案,具有指数时间复杂度。
2014-04-30 cs.FL cs.LO
Alternating Weak Automata from Universal Trees
给出了一种改进的从无限字上的交替奇偶自动机到交替弱自动机的转换。状态数的爆破与最小泛序树的大小有关,因此它是拟多项式的,并且只有当渐近优先数是状态数的对数时才是多项式的。这是对Kupferman和Vardi(2001)的翻译的指数改进,以及对Boker和Lehtinen(2018)的翻译的准多项式改进。任何稍微好一点的翻译都会(如果-像所有目前已知的这样的翻译-它是有效的建设性)导致算法解决奇偶游戏是渐近更快的最坏情况下比目前的最先进的(Calude,Jain,Khoussainov,Li和Stephan,2017; Jurdzienski和Lazić,2017;和Fearnley,Jain,Schewe,Stephan和Wojtczak,2017),因此它将产生重大突破。
2019-07-04 cs.FL
Reachability Problem for Weak Multi-Pushdown Automata
本文研究了多下推自动机的一个受限子类的可达性分析。我们假设自动机的控制状态是偏序的,并且自动机的所有转换都是相对于顺序向下的。我们证明了可达性问题的可判定性和向后可达集的可计算性。作为主要的贡献,我们确定相关的子类的可达性问题成为NP完全。这与无通信向量加法系统(无状态多下推自动机的特殊情况)的相同问题的复杂性相匹配。
2013-09-20 cs.FL cs.LO
From Muller to Parity and Rabin Automata: Optimal Transformations Preserving (History) Determinism
本文提出基于交替循环分解的两种最优变换,将 Muller 自动机分别转换为等价的确定性 parity 自动机和历史确定性 Rabin 自动机,并给出相关结构刻画与范式研究。
2024-04-19 cs.FL cs.LO
Cost Preserving Bisimulations for Probabilistic Automata
概率自动机构成了并发概率系统的通用和优雅的模型。他们配备了一个组合理论支持抽象,使弱概率互模拟作为参考概念,总结抽象的效果。本文考虑了增加成本的概率自动机。它扩展了概率自动机中弱转换的概念,使得沿着弱转换产生的成本被捕获。这就产生了成本保持和成本约束的变化弱概率双相似性,我们建立组合属性相对于并行组合。此外,多项式时间的决策算法,提出了,可以有效地用于计算马尔可夫决策过程中的组合方式的回报约束抽象。
2015-02-16 cs.FL cs.LO
On Pebble Automata for Data Languages with Decidable Emptiness Problem
在本文中,我们研究了卵石自动机(PA)的一个子类的数据语言的空性问题是可判定的。也就是说,我们引入了所谓的顶视弱PA。粗略地说,俯视图弱PA是仅在最近放置的两个卵石看到的数据值之间执行相等性测试的弱PA。这个模型的空性问题是可判定的。我们还表明,它是强大的:交替,不确定性和确定性的顶视图弱PA具有相同的识别能力。此外,该模型是强大的,足以接受所有的数据语言表示的线性时序逻辑与未来的时间运营商,增加了一个寄存器冻结量词。
2009-10-30 cs.FL
Weak Singular Hybrid Automata
Indian Institute of Technology - Bombay(印度孟买理工学院)
本文研究弱奇异混合自动机,证明其可达性问题为NP完全,LTL模型检验为PSPACE完全,并探讨扩展后的问题不确定性。
2014-06-19 cs.CC cs.FL cs.SY
On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases
本文研究了有限自动机识别位置符号编码的实数集的表达能力。我们考虑Muller自动机以及弱确定性自动机的限制类,在实际应用中用作符号集表示。在以前的工作中,已经建立了弱确定性自动机在两个不共享同一组素因子的基础上可识别的数字集合正是那些在实数和整数的一阶加法理论中可定义的数字。这一结果扩展了Cobham定理,该定理描述了可由多个基中的有限自动机识别的整数集合。在这篇文章中,我们首先将这个结果推广到乘法独立基,这使得它更接近于Cobham定理的原始陈述。然后,我们研究了Muller自动机在两个基上可识别的实数集。我们用一个反例表明,在这种情况下,科巴姆定理并不推广到乘法独立的基础。最后,我们证明了Muller自动机在两个基上可识别的实数集,如果它们不具有相同的素因子集,那么它们就是在实数和整数的一阶加法理论中可定义的实数集.因此,这些集合也可以被弱确定性自动机识别。这一结果导致了一个精确的特征集的实数是可识别的多个基地,并提供了一个理论上的理由使用弱自动机作为符号表示集。
2010-02-24 cs.FL cs.LO
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
在80年代中期,Lichelman,Pnueli和Zuck证明了一个经典定理,说明Past LTL的每个公式(带有过去算子的LTL的扩展)都等价于$\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} φ_i \vee \mathbf{F}\mathbf{G} ψ_i$形式的公式,其中$φ_i$和$ψ_i$只包含过去算子。几年后,Chang、Manna和Pnueli在这个结果的基础上导出了LTL的类似范式。这两个规范化过程都有一个非初等的最坏情况爆破,并遵循从公式到无计数器自动机到无星正则表达式再回到公式的相关路径。我们在这两点上都有所改进。我们提出了一个直接的和纯粹的语法规范化程序LTL产生一个范式,相当于一个由张,曼纳,和Pnueli,只有一个单一的指数爆破。作为一个应用,我们推导出一个简单的算法,将LTL转换成确定性的拉宾自动机。该算法规范化的公式,将其转换成一个特殊的非常弱的交替自动机,并适用于一个简单的determinisation程序,有效的只有这些特殊的自动机。
2020-05-01 cs.FL cs.LO
Featured Team Automata
我们提出了特色团队自动机,以支持团队的发展和分析,这是根据指定的同步类型进行通信的反应组件系统的变化。一个特色团队自动机简明地描述了由特征选择确定的特定配置的一系列具体产品模型。我们专注于通信安全属性的分析,但这样做很快就变得不切实际。因此,我们研究如何提升概念的接受性(没有信息丢失)的家庭模型的水平。我们发现,特色团队自动机的特色(弱)接受性的特点(弱)接受性的所有产品实例。一个原型工具支持开发的理论。
2021-08-03 cs.FL cs.MA
Büchi automata recognizing sets of reals definable in first-order logic with addition and order
这项工作考虑弱确定性Büchi自动机阅读编码的非负实数在一个固定的基地。实数自动机是一种自动机,它可以识别一组实数的所有元素的编码。它解释了如何决定在线性时间是否一组reals承认一个给定的最小弱确定性RNA是${FO}[\mathbb R;+,<,1]$ -可定义的。此外,它解释了如何计算在准二次(分别,准线性)时间存在(分别,存在普遍)${FO}[\mathbb R;+,<,1]$ -公式,定义了一套真正的自动机。它还表明,由Muchnik和Honkala的自动机在向量的自然数的技术也适用于向量的实数。这意味着一些问题,如判定实数元组集$R\subseteq\mathbb R^{d}$是否是$(\mathbb R^{d},+)$的子半群或是否是${FO}[\mathbb R;+,<,1]$ -可定义的,是可判定的.
2016-11-11 cs.FL
Weak Muller Conditions Make Delay Games Hard
我们证明了在确定性弱Muller自动机和非确定性弱Muller自动机给出的获胜条件下求解延迟对策分别是2 EXPTIME-完全和3EXPTIME-完全的。此外,双重和三重指数前瞻是必要的,足以赢得这样的游戏。这些结果是第一个表明,用于指定获胜条件的自动机类型的简洁性对这些问题的复杂性有影响。
2022-10-19 cs.FL cs.LO
Degrees of Restriction for Two-Dimensional Automata
一个三路(分别是,双向)二维的【形】自动机具有在三个方向(分别,2)由输入字母表的符号标记的单元的有限阵列上的方向。限制二维的【形】自动机的输入头部移动会导致识别能力较弱的模型。在本文中,我们引入了二维的【形】自动机的“限制度”的概念,我们开发了一套扩展的二维的【形】自动机模型,允许一些有限数量的限制移动。我们建立识别层次的确定性和非确定性扩展的三路二维的【形】自动机,我们发现类似的层次的确定性和非确定性扩展的双向二维的【形】自动机。我们还证明了不确定性和确定性的扩展三路二维的【形】自动机之间的不可比性结果。最后,我们考虑了扩展的三维二维的【形】自动机识别的语言上的一些操作的闭包性质。
2021-05-03 cs.FL
Weak Mso with the Unbounding Quantifier
本文引入了一类新的无限词语言,称之为极大正则语言,它是对$ω$ -正则语言类的扩充.这个类有两个等价的描述:自动机(一种确定性计数器自动机)和逻辑(带有边界量词的弱一元二阶逻辑)。给出了逻辑和自动机之间的有效转换。
2009-02-06 cs.FL cs.LO
The Roles of Advice to One-Tape Linear-Time Turing Machines and Finite Automata
我们讨论的权力和限制的各种“建议”,特别是弱计算模型的一个磁带线性时间图灵机和单向有限(状态)自动机。在各种建议类型中,我们考虑确定性选择的建议(不一定是算法确定的)和随机选择的建议(根据某些概率分布)。特别是,我们表明,某些薄弱的机器可以显着提高计算能力时,提供随机化的建议,而不是确定性的意见。
2010-07-18 cs.CC cs.FL
Topological transitivity of group cellular automata is decidable
Liceo “A. Einstein,” Rimini, Italy(里米尼 A·爱因斯坦中学);Department of Informatics, Systems and Communication, University of Milano-Bicocca, Italy(米兰比可卡大学信息、系统与通信系);Department of Computer Science and Engineering, University of Bologna, Campus of Cesena, Italy(博洛尼亚大学切塞纳校区计算机科学与工程系)
本文证明了任意有限群上的d维群细胞自动机的拓扑transitivity是可判定的,并由此得到若干相关动力学性质的可判定性。
2026-01-22 cs.DM cs.FL math.DS
Equivalence checking for weak bi-Kleene algebra
本文刻画了允许语言等价性判定的Pomset自动机片段,证明其与序列有理表达式对应,从而给出序列有理表达式等价性可判定的新证明。
2021-08-11 cs.FL
Conjugacy of one-dimensional one-sided cellular automata is undecidable
如果两个元胞自动机之间存在移位交换共轭,则它们是强共轭的。我们证明了以下两组一维单边元胞自动机对$(F,G)$在全移位上是递归不可分的:(i)$F$具有严格大于$G$的拓扑熵的对,和(ii)强共轭且拓扑熵为零的对.由于不存在从低熵系统到高熵系统的因子映射,也不存在高熵系统嵌入到低熵系统中,我们还得到了以下判定问题是不可判定的推论:给定两个一维单侧元胞自动机$F$和$G$在一个全移位上:$F$和$G$是共轭的吗?$F$是$G$的一个因子吗?$F$是$G$的子系统吗?所有这些在强变式和弱变式中都是不可判定的(不管同态是否需要与移位交换)。它也立即遵循这些结果举行一维双边细胞自动机。
2017-10-23 cs.CC cs.FL math.DS