如果你也在 怎样代写理论计算机theoretical computer science这个学科遇到相关的难题，请随时右上角联系我们的24/7代写客服。
理论计算机科学在精神上是数学的和抽象的，但它的动机来自于实际和日常的计算。它的目的是理解计算的本质，并作为这种理解的结果，提供更有效的方法论。
statistics-lab™ 为您的留学生涯保驾护航 在代写理论计算机theoretical computer science方面已经树立了自己的口碑, 保证靠谱, 高质且原创的统计Statistics代写服务。我们的专家在代写理论计算机theoretical computer science代写方面经验极为丰富，各种代写理论计算机theoretical computer science相关的作业也就用不着说。
我们提供的理论计算机theoretical computer science及其相关学科的代写，服务范围广, 其中包括但不限于:
- Statistical Inference 统计推断
- Statistical Computing 统计计算
- Advanced Probability Theory 高等概率论
- Advanced Mathematical Statistics 高等数理统计学
- (Generalized) Linear Models 广义线性模型
- Statistical Machine Learning 统计机器学习
- Longitudinal Data Analysis 纵向数据分析
- Foundations of Data Science 数据科学基础
数学代写|理论计算机代写theoretical computer science代考|Introduction
Model checking is a formal approach for verifying quantitative and qualitative properties of computer systems. In this way, the system is modelled by a labelled transition system, and its properties are specified in temporal logic. Because of some stochastic behaviours of these systems, we can use probabilistic model checking to analyse the quantitative property specifications of these systems [1-3]. In this domain, we can use discrete and continuous time Markov Chains to model fully probabilistic systems. Besides, Markov Decision Processes [5] are used to model systems with both probabilistic and non-deterministic behaviours. Probabilistic Computation Tree Logic (PCTL) [1] is used to formally specify the
related system properties. A main part of PCTL properties against MDPs can be verified by computing the extremal reachability probability: The maximal or minimal probability of reaching a given set of goal states. For quantitative parts, numerical computations are needed to calculate these reachability probabilities $[2,6]$. Linear programming $[1,3]$, value iteration and policy iteration are wellknown numerical approaches for computing the optimal reachability probabilities $[2,5]$. PRISM [4] and STORM [7] are examples of probabilistic model checkers that use these numerical methods to compute reachability probabilities.
One of the main challenges of model checking in all variants is the state space explosion problem, i.e., the excessive space requirement to store the states of the model in the memory $[1,9]$. For probabilistic model checking, we have the additional difficulty of solving linear programs. For the feasibility of the algorithms we need efficient heuristics to decrease the running time of these algorithms [3]. A wide range of approaches has been proposed for probabilistic model checking in previous works to tackle these problems. Symbolic model checking [9], compositional verification [10], symmetry reduction for probabilistic systems $[11]$, incremental model construction [12] and statistical model checking [6] have been proposed to reduce the needed space for probabilistic model checking. In addition, several approaches are used to accelerate standard algorithms for probabilistic model checking. SCC-based approaches $[13,14]$ identify strongly connected components (SCCs) of the underlying model and compute reachability probabilities of the states of each component in a right order. Learning based algorithms use the idea of real-time dynamic programming to solve reachability probability problems of MDPs [15]. Prioritization methods focus on finding a good state ordering to update the values of states during iterative computations $[13,14]$. The idea of finding Maximal End Components (MECs) is used in [3] to reduce the number of states of the model. Several techniques are proposed in [17] to reduce the size of a DTMC model. These techniques are used to reduce the model for finite-horizon properties.
数学代写|理论计算机代写theoretical computer science代考|Preliminaries
In this section, we provide an overview of DTMCs and MDPs and reachability properties. We mainly follow the notations of $[1,13]$. Let $S$ be a countable set. A discrete probability distribution on $S$ is a function $P: S \rightarrow[0,1]$ satisfying $\sum_{s \in S} P(s)=1$. We use $\operatorname{Dist}(S)$ as the set of all distributions on $S$. The support of $P$ is defined as the set $S u p p(P)={s \in S \mid P(s)>0}$. A distribution $P$ is Dirac if $S u p p(P)$ has only one member. More details about the proposed definitions in this section and their related probability measures are available in $[1,2,16]$.
Definition 1. A Discrete-time Markov Chain (DTMC) is a tuple $D=(S, \hat{s}$, $\mathbf{P}, R, G$ ) where $S$ is a countable, non-empty set of states, $\hat{s} \in S$ is the initial state, $\mathbf{P}: S \times S \rightarrow[0,1]$ is the probabilistic transition function, $R: S \times S \rightarrow \Re_{\geq 0}$ is a reward function wich assigns to each transition of $P$ a non-negative reward value and $G \subseteq S$ is the set of Goal states.
A DTMC $D$ is called finite if $S$ is finite. For a finite $D$, size $(D)$ is the number of states of $D$ plus the number of transitions of the form $\left(s, s^{\prime}\right) \in S \times S$ with $\mathbf{P}$ $\left(s, s^{\prime}\right)>0$. A path represents a possible execution of $D[2]$ and is a non-empty (finite or infinite) sequence of states $s_{0} s_{1} s_{2} \ldots$ such that $\mathbf{P}\left(s_{i}, s_{i+1}\right)>0$ for all $i \geq 0$. We use $P_{a t h s_{D, s}}$ to denote the set of all paths of $D$ that start in the state $s$ and we use FPaths ${ }{D, s}$ for the subset of finite paths of $P{a t h} s_{D, s}$. We also use Path $s_{D}$ and FPaths $_{D}$ for $\cup_{s \in S} P a t h s_{D, s}$ and $\cup_{s \in S} F P a t h s_{D, s}$ respectively. For a finite path $\pi=s_{0} s_{1} \ldots s_{k}$, the accumulated reward is defined as: $\sum_{i<k} R\left(s_{i}, s_{i+1}\right)$. For an infinite path $\pi=s_{0} s_{1} \ldots$ and for every $j \geq 0$, let $\pi[j]=s_{j}$ denote the $(j+1)$ th state of $\pi$ and $\pi[. . j]$ the $(j+1)$ th prefix of the form $s_{0} s_{1} \ldots s_{j}$ of $\pi$. We use pref $(\pi)$ as the set of all prefixes of $\pi$.
数学代写|理论计算机代写theoretical computer science代考|Probability Measure of a Markov Chain
In order to reason about the behaviour of a Markov chain $D$, we need to formally use the cylinder sets of the finite paths of $D[1]$.
Definition 2. The Cylinder set of a finite path $\hat{\pi} \in F P a$ h.s $_{D}$ is defined as $\operatorname{Cyl}(\hat{\pi})=\left{\pi \in\right.$ Paths $\left.{D} \mid \hat{\pi} \in \operatorname{pre} f(\pi)\right}$. The probability measure $\operatorname{Pr}^{D}$ is defined on the cylinder sets as $P r^{D}\left(C y l\left(s{0} \ldots s_{n}\right)\right)=\prod_{0 \leq i<n} \mathbf{P}\left(s_{i}, s_{i+1}\right)$.
Markov Decision Processes (MDPs) are a generalization of DTMCs that are used to model systems that have a combination of probabilistic and non-deterministic behaviour. An MDP is a tuple $M=(S, \hat{s}$, Act, $\delta, R, G)$ where $S, \hat{s}$ and $G$ are the same as for DTMCs, Act is a finite set of actions, $R: S \times A c t \times S \rightarrow \Re_{\geq 0}$ is a reward function, assigns to each transition a non-negative reward value and $\delta: S \times A c t \rightarrow \operatorname{Dist}(S)$ is a probabilistic transition function. For every state $s \in S$ of an MDP $M$ one or more actions of Act are defined as enabled actions. We use $A c t(s)$ for this set and define it as $\operatorname{Act}(s)={\alpha \in A c t \mid \delta(s, \alpha)$ is defined $}$.
For $s \in S$ and $\alpha \in \operatorname{Act}(s)$ we use Post $(s, \alpha)$ for the set of $\alpha$ successors of $s$, Post $(s)$ for all successors of $s$ and Pre $(s)$ for predecessors of $s[1]$ :
$$
\begin{aligned}
&\operatorname{Post}(s, \alpha) \doteq\left{s^{\prime} \in S \mid \delta\left(s, \alpha, s^{\prime}\right)>0\right} \
&\operatorname{Post}(s) \doteq \cup_{\alpha \in \operatorname{Act}(s)} \operatorname{Post}(s, \alpha),
\end{aligned}
$$
To evaluate the operational behaviour of an MDP $M$ we should consider two steps to take a transition from a state $s \in S$. First, one enabled action $\alpha \in \operatorname{Act}(s)$ is chosen non-deterministically. Second, according to the probability distribution $\delta(s, \alpha)$, a successor state $s^{\prime} \in \operatorname{Post}(s, \alpha)$ is selected randomly. In this case, $\delta(s, \alpha)\left(s^{\prime}\right)$ determines the probability of a transition from $s$ to $s^{\prime}$ by the action $\alpha \in \operatorname{Act}(s)$. We extend the definition of paths for MDPs: A path in an MDP $M$ is a non-empty (finite or infinite) sequence $\pi=s_{0} \stackrel{\alpha_{0}}{\rightarrow} s_{1} \stackrel{\alpha_{1}}{\rightarrow} \ldots$ where $s_{i} \in S$ and $\alpha_{i} \in \operatorname{Act}\left(s_{i}\right)$ and $s_{i+1} \in \operatorname{Post}\left(s_{i}, \alpha_{i}\right)$ for every $i \geq 0$. Similar to the case with DTMCs, for a state $s \in S$, we use Paths $_{M, s}$ to denote the set of all paths of $M$ starting in $s$ and $F$ Paths ${ }_{M, s}$ for all finite paths of it. For reasoning about the probabilistic behaviour of an MDP we use the notion of policy (also called adversary) $[2,3,6]$.
Definition 3. A (deterministic) policy of an MDP $M$ is a function $\sigma$ : FPath $_{M} \rightarrow$ Act that for every finite path $\pi=s_{0} \stackrel{\alpha_{0}}{\rightarrow} s_{1} \stackrel{\alpha_{i}}{\rightarrow} \ldots \stackrel{\alpha_{i-1}}{\rightarrow} s_{i}$ selects an enabled action $\alpha_{i} \in \operatorname{Act}\left(s_{i}\right)$. The policy $\sigma$ is memoryless if it depends only on the last state of the path. In general, a policy is defined as function of $F P a t h_{M}$ to a distribution on Act. However, memoryless and deterministic policies are enough for computing the optimal unbounded reachability probabilities [2]. We use $\mathrm{Pol}{M}$ for the set of all deterministic and memoryless policies of $M$. A policy $\sigma \in \operatorname{Pol}{M}$ resolves all non-deterministic choices in $M$ and induces a DTMC $M^{\sigma}$ for which every state is a finite path of $M$.
理论计算机代写
数学代写|理论计算机代写theoretical computer science代考|Introduction
模型检查是一种用于验证计算机系统的定量和定性属性的正式方法。通过这种方式，系统由标记的转换系统建模，并且其属性在时间逻辑中指定。由于这些系统的一些随机行为，我们可以使用概率模型检查来分析这些系统的定量属性规范 [1-3]。在这个领域，我们可以使用离散和连续时间马尔可夫链来模拟完全概率系统。此外，马尔可夫决策过程 [5] 用于对具有概率和非确定性行为的系统进行建模。概率计算树逻辑 (PCTL) [1] 用于正式指定
相关的系统属性。针对 MDP 的 PCTL 属性的主要部分可以通过计算极值可达性概率来验证：达到给定目标状态集的最大或最小概率。对于定量零件，需要进行数值计算来计算这些可达性概率[2,6]. 线性规划[1,3]，值迭代和策略迭代是计算最优可达概率的著名数值方法[2,5]. PRISM [4] 和 STORM [7] 是概率模型检查器的示例，它们使用这些数值方法来计算可达概率。
在所有变体中进行模型检查的主要挑战之一是状态空间爆炸问题，即将模型状态存储在内存中的空间需求过多[1,9]. 对于概率模型检查，我们有解决线性规划的额外困难。为了算法的可行性，我们需要有效的启发式方法来减少这些算法的运行时间[3]。在以前的工作中已经提出了多种方法来进行概率模型检查以解决这些问题。符号模型检查 [9]、组合验证 [10]、概率系统的对称性降低[11]、增量模型构建 [12] 和统计模型检查 [6] 已被提出以减少概率模型检查所需的空间。此外，几种方法用于加速概率模型检查的标准算法。基于 SCC 的方法[13,14]识别底层模型的强连接组件 (SCC)，并以正确的顺序计算每个组件状态的可达性概率。基于学习的算法使用实时动态规划的思想来解决 MDP [15] 的可达性概率问题。优先级方法专注于在迭代计算期间找到一个好的状态排序来更新状态的值[13,14]. [3] 中使用了寻找最大末端组件 (MEC) 的想法来减少模型的状态数量。[17] 中提出了几种技术来减小 DTMC 模型的大小。这些技术用于减少有限范围属性的模型。
数学代写|理论计算机代写theoretical computer science代考|Preliminaries
在本节中，我们概述了 DTMC 和 MDP 以及可达性属性。我们主要遵循以下符号[1,13]. 让小号是可数集。离散概率分布小号是一个函数磷:小号→[0,1]令人满意的∑s∈小号磷(s)=1. 我们用区(小号)作为所有分布的集合小号. 的支持磷被定义为集合小号在pp(磷)=s∈小号∣磷(s)>0. 一个分布磷是狄拉克如果小号在pp(磷)只有一个成员。有关本节中提出的定义及其相关概率度量的更多详细信息，请参见[1,2,16].
定义 1. 离散时间马尔可夫链 (DTMC) 是一个元组D=(小号,s^, 磷,R,G） 在哪里小号是可数的非空状态集，s^∈小号是初始状态，磷:小号×小号→[0,1]是概率转移函数，R:小号×小号→ℜ≥0是分配给每个转换的奖励函数磷非负奖励值和G⊆小号是目标状态的集合。
一个DTMCD称为有限如果小号是有限的。对于一个有限D， 尺寸(D)是状态数D加上表格的转换次数(s,s′)∈小号×小号和磷 (s,s′)>0. 路径表示可能的执行D[2]并且是非空（有限或无限）状态序列s0s1s2…这样磷(s一世,s一世+1)>0对全部一世≥0. 我们用磷一种吨HsD,s表示所有路径的集合D从该州开始s我们使用 FPathsD,s对于有限路径的子集磷一种吨HsD,s. 我们也使用路径sD和 FPathsD为了∪s∈小号磷一种吨HsD,s和∪s∈小号F磷一种吨HsD,s分别。对于有限路径圆周率=s0s1…sķ，累积奖励定义为：∑一世<ķR(s一世,s一世+1). 对于无限路径圆周率=s0s1…并且对于每个j≥0， 让圆周率[j]=sj表示(j+1)的状态圆周率和圆周率[..j]这(j+1)表格的 th 前缀s0s1…sj的圆周率. 我们使用首选(圆周率)作为所有前缀的集合圆周率.
数学代写|理论计算机代写theoretical computer science代考|Probability Measure of a Markov Chain
为了推理马尔可夫链的行为D，我们需要正式使用有限路径的柱面集D[1].
定义 2. 有限路径的圆柱集圆周率^∈F磷一种hsD定义为\operatorname{Cyl}(\hat{\pi})=\left{\pi \in\right.$ 路径 $\left.{D} \mid \hat{\pi} \in \operatorname{pre} f( \pi)\右}\operatorname{Cyl}(\hat{\pi})=\left{\pi \in\right.$ 路径 $\left.{D} \mid \hat{\pi} \in \operatorname{pre} f( \pi)\右}. 概率测度公关D在气缸组上定义为磷rD(C是l(s0…sn))=∏0≤一世<n磷(s一世,s一世+1).
马尔可夫决策过程 (MDP) 是 DTMC 的概括，用于对具有概率和非确定性行为组合的系统进行建模。MDP 是一个元组米=(小号,s^， 行为，d,R,G)在哪里小号,s^和G与 DTMC 相同，Act 是一组有限的动作，R:小号×一种C吨×小号→ℜ≥0是一个奖励函数，为每个转换分配一个非负奖励值，并且d:小号×一种C吨→区(小号)是一个概率转移函数。对于每个州s∈小号一个 MDP 的米Act 的一个或多个动作被定义为启用的动作。我们用一种C吨(s)对于这个集合并将其定义为行为(s)=一种∈一种C吨∣d(s,一种)$一世sd和F一世n和d$.
为了s∈小号和一种∈行为(s)我们使用邮政(s,一种)对于一组一种继任者s， 邮政(s)对于所有继任者s和预(s)对于前辈s[1] :
\begin{aligned} &\operatorname{Post}(s, \alpha) \doteq\left{s^{\prime} \in S \mid \delta\left(s, \alpha, s^{\prime}\ right)>0\right} \ &\operatorname{Post}(s) \doteq \cup_{\alpha \in \operatorname{Act}(s)} \operatorname{Post}(s, \alpha), \end{对齐}\begin{aligned} &\operatorname{Post}(s, \alpha) \doteq\left{s^{\prime} \in S \mid \delta\left(s, \alpha, s^{\prime}\ right)>0\right} \ &\operatorname{Post}(s) \doteq \cup_{\alpha \in \operatorname{Act}(s)} \operatorname{Post}(s, \alpha), \end{对齐}
评估 MDP 的操作行为米我们应该考虑两个步骤来从一个状态转换s∈小号. 首先，一个启用的动作一种∈行为(s)是非确定性地选择的。二、根据概率分布d(s,一种), 后继状态s′∈邮政(s,一种)是随机选择的。在这种情况下，d(s,一种)(s′)确定从s到s′通过行动一种∈行为(s). 我们扩展了 MDP 的路径定义： MDP 中的路径米是一个非空（有限或无限）序列圆周率=s0→一种0s1→一种1…在哪里s一世∈小号和一种一世∈行为(s一世)和s一世+1∈邮政(s一世,一种一世)对于每个一世≥0. 与 DTMC 的情况类似，对于一个状态s∈小号，我们使用路径米,s表示所有路径的集合米开始于s和F路径米,s对于它的所有有限路径。为了推理 MDP 的概率行为，我们使用策略（也称为对手）的概念[2,3,6].
定义 3. MDP 的（确定性）策略米是一个函数σ: 路径米→对每条有限路径采取行动圆周率=s0→一种0s1→一种一世…→一种一世−1s一世选择一个启用的动作一种一世∈行为(s一世). 政策σ如果它仅取决于路径的最后状态，则它是无记忆的。一般来说，策略被定义为F磷一种吨H米对法案的分配。然而，无记忆和确定性策略足以计算最佳无界可达概率[2]。我们用磷这l米对于所有确定性和无记忆策略的集合米. 一项政策σ∈波尔米解决所有非确定性选择米并诱导 DTMC米σ其中每个状态都是一条有限路径米.
统计代写请认准statistics-lab™. statistics-lab™为您的留学生涯保驾护航。
金融工程代写
金融工程是使用数学技术来解决金融问题。金融工程使用计算机科学、统计学、经济学和应用数学领域的工具和知识来解决当前的金融问题，以及设计新的和创新的金融产品。
非参数统计代写
非参数统计指的是一种统计方法，其中不假设数据来自于由少数参数决定的规定模型；这种模型的例子包括正态分布模型和线性回归模型。
广义线性模型代考
广义线性模型（GLM）归属统计学领域，是一种应用灵活的线性回归模型。该模型允许因变量的偏差分布有除了正态分布之外的其它分布。
术语 广义线性模型（GLM）通常是指给定连续和/或分类预测因素的连续响应变量的常规线性回归模型。它包括多元线性回归，以及方差分析和方差分析（仅含固定效应）。
有限元方法代写
有限元方法（FEM）是一种流行的方法，用于数值解决工程和数学建模中出现的微分方程。典型的问题领域包括结构分析、传热、流体流动、质量运输和电磁势等传统领域。
有限元是一种通用的数值方法，用于解决两个或三个空间变量的偏微分方程（即一些边界值问题）。为了解决一个问题，有限元将一个大系统细分为更小、更简单的部分，称为有限元。这是通过在空间维度上的特定空间离散化来实现的，它是通过构建对象的网格来实现的：用于求解的数值域，它有有限数量的点。边界值问题的有限元方法表述最终导致一个代数方程组。该方法在域上对未知函数进行逼近。[1] 然后将模拟这些有限元的简单方程组合成一个更大的方程系统，以模拟整个问题。然后，有限元通过变化微积分使相关的误差函数最小化来逼近一个解决方案。
tatistics-lab作为专业的留学生服务机构，多年来已为美国、英国、加拿大、澳洲等留学热门地的学生提供专业的学术服务，包括但不限于Essay代写，Assignment代写，Dissertation代写，Report代写，小组作业代写，Proposal代写，Paper代写，Presentation代写，计算机作业代写，论文修改和润色，网课代做，exam代考等等。写作范围涵盖高中，本科，研究生等海外留学全阶段，辐射金融，经济学，会计学，审计学，管理学等全球99%专业科目。写作团队既有专业英语母语作者，也有海外名校硕博留学生，每位写作老师都拥有过硬的语言能力，专业的学科背景和学术写作经验。我们承诺100%原创，100%专业，100%准时，100%满意。
随机分析代写
随机微积分是数学的一个分支，对随机过程进行操作。它允许为随机过程的积分定义一个关于随机过程的一致的积分理论。这个领域是由日本数学家伊藤清在第二次世界大战期间创建并开始的。
时间序列分析代写
随机过程，是依赖于参数的一组随机变量的全体，参数通常是时间。 随机变量是随机现象的数量表现，其时间序列是一组按照时间发生先后顺序进行排列的数据点序列。通常一组时间序列的时间间隔为一恒定值（如1秒，5分钟，12小时，7天，1年），因此时间序列可以作为离散时间数据进行分析处理。研究时间序列数据的意义在于现实中，往往需要研究某个事物其随时间发展变化的规律。这就需要通过研究该事物过去发展的历史记录，以得到其自身发展的规律。
回归分析代写
多元回归分析渐进（Multiple Regression Analysis Asymptotics）属于计量经济学领域，主要是一种数学上的统计分析方法，可以分析复杂情况下各影响因素的数学关系，在自然科学、社会和经济学等多个领域内应用广泛。
MATLAB代写
MATLAB 是一种用于技术计算的高性能语言。它将计算、可视化和编程集成在一个易于使用的环境中，其中问题和解决方案以熟悉的数学符号表示。典型用途包括：数学和计算算法开发建模、仿真和原型制作数据分析、探索和可视化科学和工程图形应用程序开发，包括图形用户界面构建MATLAB 是一个交互式系统，其基本数据元素是一个不需要维度的数组。这使您可以解决许多技术计算问题，尤其是那些具有矩阵和向量公式的问题，而只需用 C 或 Fortran 等标量非交互式语言编写程序所需的时间的一小部分。MATLAB 名称代表矩阵实验室。MATLAB 最初的编写目的是提供对由 LINPACK 和 EISPACK 项目开发的矩阵软件的轻松访问，这两个项目共同代表了矩阵计算软件的最新技术。MATLAB 经过多年的发展，得到了许多用户的投入。在大学环境中，它是数学、工程和科学入门和高级课程的标准教学工具。在工业领域，MATLAB 是高效研究、开发和分析的首选工具。MATLAB 具有一系列称为工具箱的特定于应用程序的解决方案。对于大多数 MATLAB 用户来说非常重要，工具箱允许您学习和应用专业技术。工具箱是 MATLAB 函数（M 文件）的综合集合，可扩展 MATLAB 环境以解决特定类别的问题。可用工具箱的领域包括信号处理、控制系统、神经网络、模糊逻辑、小波、仿真等。